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 a standalone command-line application for MacOS and Linux (Ubuntu 18.04 and 20.04), with Windows Cygwin in progress.
The OpenJML command line tool is OS-dependent. Download the appropriate release from the github latest release page.
The download retrieves a .zip file. Unzip the file into a new directory of your choice (call it $OJ). $OJ should contain the `openjml` executable and other files and folders. Some browsers or download utilities will automatically unzip the .zip file for you, leaving an unzipped folder in your downloads folder. You can move or rename the folder (with all its contents) to a location of your choice.
These are the particularly relevant files in the top-level of the installation folder:
If $OJ is the installation directory, then you can run openjml using the command line $OJ/openjml. For example, $OJ/openjml -version will emit the version number of this build.
Further instructions about running OpenJML can be found here.
OpenJML uses SMT solvers as logic checkers. A selection of supported solvers is bundled with the OpenJML release.