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

• TiagoAlves
• PauloSilva

AVAILABILITY

The source code of VooDooM can be obtained from its sourceforge project page:

• http://sourceforge.net/projects/voodoom/

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.