ViennaTalk

ViennaTalk is a VDM environment built upon Pharo Smalltalk system.

Pre-built packages for MacOSX, Linux and Windows are available at https://github.com/tomooda/ViennaTalk-doc/releases.

Demo movies

VDMPad

VDMPad is a lightweight WebIDE for VDM-SL shipped with ViennaTalk.

A free VDMPad server is available by courtesy of Kyushu University, Japan. No user registration is required.

VDMTools

VDMTools is a fully featured toolbox for VDM-family with a long history. It has both IDE with GUI and command line tools with features including syntax checkers, type checkers, interpreters, proof obligation generators and code generators. Binary packages (for Mac, Linux and Windows) and documentation (in English and Japanese) are available at fmvdm site, and all source code and documentation are now open-sourced under GPLv3 at github repository.

vdm-mode

vdm-mode is an Emacs package for writing VDM specifications using VDM-SL, VDM++ and VDM-RT.

VDMJ

Description

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 Overture project, which adds a graphical Eclipse IDE interface as well as features like code generation (see screen shots below).

Features

• 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