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
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:
The OpenJML command line tool may be downloaded via the green download link button, below.
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.
The Update site for the Eclipse plug-in that encapsulates the OpenJML tool is http://jmlspecs.sourceforge.net/openjml-updatesite.