/vdmj

Formal Modelling in VDM

Primary LanguageJavaGNU General Public License v3.0GPL-3.0

Fujitsu LogoVDMJ

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. It is also accessible via the LSP/DAP protocols and can be used by an IDE like VS Code (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

Documentation

  • User Guide
  • One Page Guide
  • High Precision Guide
  • VDMJUnit Guide
  • Annotation Guide
  • Library Guide
  • External Format Guide
  • Plugin Writer's Guide

Screen Shots

Eclipse Integration VS Code Integration Help Precondition failure VDMJUnit High Precision