: A transformation tool for VDM-SL.
reads VDM-SL specifications and applies transformation rules to
the datatypes that are defined in them to obtain a relational
representation for these datatypes. The relational representation can be
- VDM-SL datatypes (inserted back into the original specification)
- SQL table definitions (can be fed to a relational DBMS)
at the command line, and follow instructions.
-i Input file --input=Input file VDM input file
-v VDM Output file --vdm=VDM Output file VDM Output File
-s SQL Output file --sql=SQL Output file SQL output file
-h --help Show this help screen
The source code of VooDooM
can be obtained from its sourceforge project page:
makes use of the parsing, pretty-printing, and traversal support for VDM-SL provided by VooDooMFront
. This means that VooDooM
uses a VDM-SL grammar specified in SDF together with Haskell modules generated from this grammar using the Sdf2Haskell?
tool of the Strafunski bundle.
The relational calculus implemented by VooDooM
is described in the following paper:
- Tiago Alves, Paulo Silva, Joost Visser, and José Nuno Oliveira. Strategic Term Rewriting And Its Application To A VDM-SL to SQL Conversion. Formal Methods 2005, Springer©, to appear. (pdf)
In addition to the calculus itself, the paper descibes the use of strategic programming in its implementation, using the Haskell-based Strafunski bundle.