OpenJML is a tool for working with logical annotations in Java programs. It enables static or run-time checking of the validity of the annotations, with other features in planning.

The following software packages are available:

  • A command-line tool to do type-checking, static checking or runtime checking
  • An Eclipse plug-in which allows you to use OpenJML from within the Eclipse IDE

OpenJML (Command Line Tool)

The OpenJML command line tool may be downloaded via one of the download links, below. OpenJML has the following system requirements:
  • A modern operating system such as Windows 7, Mac OS X, or Linux capable of running Java.
  • A JDK, such as OpenJDK or Oracle's JDK (currently Java 7 only)
In order to use the static checking capabilities of OpenJML, you will need to install a theorem prover. The following provers are supported by OpenJML:
  • Z3 (version 4.3) on Windows and Mac (not quite working yet on Linux)
  • CVC4 (version 1.2) on Windows
  • Yices3 (version 2.1) on Windows or Mac OSX

Download OpenJML (All Platforms)

Eclipse Plugin (Includes OpenJML)

The Update site for the Eclipse plug-in that encapsulates the OpenJML tool is