VDMJ

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 and a proof obligation generator as well as JUnit support for automatic testing and annotation support.

VDMJ is a command line tool, but it is used by the Overture eclipse project, and the VDM VSCode extension which adds a full GUI interface. You can find the VDMJ project on GitHub. The original IPR for VDMJ is owned by my former employer, Fujitsu UK. The GitHub project is a derived work, under the GPL.

There is a wiki describing VDMJ and its documentation here.

You can find out more about the VDM specification language and its tools here:

http://en.wikipedia.org/wiki/Vienna_Development_Method

http://overturetool.org/

https://github.com/overturetool/vdm-vscode