VooDooM: A transformation tool for VDM-SL.
FUNCTIONALITY
VooDooM 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
exported as:
- VDM-SL datatypes (inserted back into the original specification)
- SQL table definitions (can be fed to a relational DBMS)
USAGE
Just type
VooDooM
at the command line, and follow instructions.
Usage:
-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
AUTHORS
AVAILABILITY
The source code of
VooDooM can be obtained from its sourceforge project page:
IMPLEMENTATION
VooDooM 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.
DOCUMENTATION
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.