The VooDooMFront package provides a grammar for VDM, written in SDF, as well as support for parsing, tree building, and tree traversal.

The grammar is based on the ISO/IEC 13817-1:1996 reference document that describes the concrete and abstract syntax of VDM-SL.

Documentation

Technical Report: Development of an Industrial Strength Grammar for VDM

The development of the VDM grammar in SDF is documented in the following technical report:

• Tiago Alves and Joost Visser, Development of an Industrial Strength Grammar for VDM. Technical Report, DI-Research.PURe-05.04.29, Departamento de Informática, Universidade do Minho, April 2005. (pdf)

The report describes the grammar engineering methodology that was applied, the tools employed, and the various stages of evolution during grammar development. In particular, the report shows metrics data collected using SdfMetz for all 48 development versions of the grammar. A pretty-printed version of the grammar is included as appendix.

Browsable grammar

A browsable HTML rendering of the VDM-SL grammar in SDF is available from:

• http://voodoom.sourceforge.net/iso-vdm.html

By clicking on non-terminal names one can easily navigate and explore the grammar structure.

Extreme Grammaring Presentation

Although parsing is a subset of a well studied area like compilers, grammars were always looked upon as "the ugly duckling". In this presentation I propose a novel methodology, baptized "Extreme Grammaring", for developing grammars using the SDF (Syntax Definition Formalism), inspired in Extreme Programming.

This methodology made possible the development of an industrial strength grammar for ISO VDM-SL, one of the most common languages used for formal specification.

"Extreme Grammaring" presentation slides (Presented on December, 21 in the PUReCafe)

Download

Version	Download	Remarks
0.0.1	tgz	Follows standard strictly. Contains ambiguities.
0.0.2	tgz	Fully disambiguated. Some deviations from standard for disambiguation purposes.
0.0.3	tgz	AST constructor names added. Some injections removed.
1.0	tgz	Haskell front-end with parsing, AST outputting and pretty-printing support.

For detailed description of each release, see the remarks below as well as the README and ChangeLog files included in each distribution.

See VDMGrammarEvolution for metric values for all versions.

Upcoming releases

• Version 2.0: This version will contain the front-end for Java, supporting parsing, tree building, and tree traversal, most probably following the JJForester approach.

Related

• VooDooM is a tool that converts VDM-SL data types to relational form, and exports them as SQL.

Credits

The main developer of VooDooMFront is:

• TiagoAlves