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.

Annotations

Direct execution plugin for PO verification.

VDMJ LSP Server

An example external file reader for CSV files

An example RemoteSimulation

Example VDM to C class mapper implementation

An example external file reader for PDF files

DBGP protocol handler for VDMJ

Annotations2

Example and useful CommandPlugin examples

Distribution packaging for key jars