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

OpenJML uses SMT solvers as logic checkers. A selection of supported solvers is bundled with the OpenJML release.

OpenJML (Command Line Tool)

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

Download OpenJML (All Platforms)

(Alternately you can use the github project releases page).

The download retrieves a .zip file. Unzip the file into a new directory of your choice (call it $OJ). $OJ should contain openjml.jar and other files. Some browsers or download utilities will automatically unzip the .zip file for you, leaving an unzipped folder in your downloads folder. You can move the folder (with all its contents) to a location of your choice.

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

Use the "Install New Software" command within the Eclipse IDE to add the OpenJML plugin to your Eclipse installation.