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