Formal Modelling in VDM

5.0 Stars (3)
44 Downloads (This Week)
Last Update:
Download vdmj-3.0.1.jar
Browse All Files
Windows Mac Linux



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).

VDMJ Web Site


  • 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

Update Notifications

User Ratings

ease 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
features 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
design 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
support 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
Write a Review

User Reviews

  • peterwvj
    1 of 5 2 of 5 3 of 5 4 of 5 5 of 5

    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.

    Posted 08/16/2013
  • leouk
    1 of 5 2 of 5 3 of 5 4 of 5 5 of 5

    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!!

    Posted 02/07/2013
  • pglvdm
    1 of 5 2 of 5 3 of 5 4 of 5 5 of 5

    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!

    Posted 10/27/2012
Read more reviews

Additional Project Details

Intended Audience

Developers, Architects, Quality Engineers

User Interface


Programming Language



Screenshots can attract more users to your project.
Features can attract more users to your project.

Icons must be PNG, GIF, or JPEG and less than 1 MiB in size. They will be displayed as 48x48 images.