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

The tool is available as either

  • a command-line Java application or
  • as an Eclipse plugin.
Information about the system requirements and installation can be found here.

SMT solvers

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

OpenJML (Command Line Tool)

The OpenJML command line tool may be downloaded via the green download link button, below.

Download OpenJML (All Platforms)

The download retrieves a .zip or .tar.gz file. Unzip or untar the file into a new directory or your choice (call it $OJ). $OJ should contain openjml.jar and other files.

You can run OpenJML by, for example, this command-line.

java -jar $OJ/openjml.jar -help

Instructions about running OpenJML can be found here.

Eclipse Plugin (Includes OpenJML)

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