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 (with arbitrary precision arithmetic), a debugger, a proof obligation generator and a combinatorial test generator with coverage recording, as well as JUnit support for automatic testing and user definable annotations.
VDMJ is a command line tool, but it is used by the project, which adds a graphical Eclipse IDE interface as well as features like code generation. It is also accessible via the LSP/DAP protocols and can be used by an IDE like
(see screen shots below).
- 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 (eg. Greek, Japanese or Cyrillic)
- Supports external libraries and remote control (tool integration)
- Provides JUnit support for automatic testing of specifications
- Supports arbitrary precision arithmetic
- Supports user defined annotations
