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
OpenJML uses SMT solvers as logic checkers. A selection of supported solvers is bundled with the OpenJML release.
The OpenJML command line tool may be downloaded via the green download link button, below.
(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.
The Update site for the Eclipse plug-in that encapsulates the OpenJML tool is http://jmlspecs.sourceforge.net/openjml-updatesite.
Use the "Install New Software" command within the Eclipse IDE to add the OpenJML plugin to your Eclipse installation.