VDMJ provides basic tool support for the VDM-SL, VDM++ and VDM-RT specification languages, written in Java. It includes a parser, a type checker, an interpreter, a debugger, a proof obligation generator and a combinatorial test generator with coverage recording, as well as JUnit support for automatic testing.
VDMJ is a command line tool, but it is used by the Overture project, which adds a graphical Eclipse IDE interface (see screen shots).
- Parses, type checks, executes and debugs VDM specifications
- Generates proof obligations
- Generates detailed code coverage for tests in LaTeX or MS doc
- Performs combinatorial tests
- Supports all three VDM dialects: VDM-SL, VDM++ and VDM-RT
- Supports plain text, LaTeX, MS doc, docx or ODF source files
- Supports international character sets in specifications
- Supports external libraries and remote control (tool integration)
- Provides JUnit support for automatic testing of specifications
In the Overture project we have developed a new architecture for the VDM Abstract Syntax Tree (AST) in order to make it easier to use the platform as a basis for developing tools for formal modeling. To validate the test outputs of the parser, type checker, interpreter, proof obligation generator etc. we compare the outputs to those produced by VDMJ. VDMJ is a very mature and high quality reference and has significantly contributed to the quality of the new Overture AST archiecture.
VDMJ is the backend of the Overture tools as the parser, typechecker, and interpreter for a variety of VDM dialects (e.g. SL, RT, ++, classic, etc). It is lean and efficient setup provides reliable accountability of VDM specifications of varied sizes. Much recommended if you want to streamline your VDM development or even integrate your own tools / code with VDM-ready features. Much recommended!!
VDMJ is an extremely will engineered core tool supporting the different VDM dialects in a very mature fashion. VDMJ forms the core of the Overture open source initiative (also on SF). Without VDMJ as the core of that Overture or the follow up initiatives such as DESTECS (also on SF) or COMPASS (also on SF) would not have been anywhere. I give VDMJ my warmest recommendations!