Formal Modelling in VDM
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 and a proof obligation generator 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
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!