JML Logo

OpenJML Installation

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; it also provides an enhanced version of javadoc that includes the annotations in the javadoc documentation.

The functionality is available

System requirements
Installation
Execution
OpenJML in Eclipse

System requirements: OS and Java

OpenJML requires

Installation - Command-line Java application

To install the command-line tool, complete these steps:

Installation - Eclipse plug-in

Installing Eclipse

Note that you need Java 8 on your system to use OpenJML through Eclipse.

You can download and install Eclipse from here. You should download the 'Eclipse IDE for Java Developers' package, version Neon.2 or later. (Other packages may do as well as long as they have support for Java development.)

Installing the plug-in

Four CAUTIONS:

To install the Eclipse plug-in, use the Eclipse mechanism for installing plug-ins from an update site, using this URL for the update site: http://jmlspecs.sourceforge.net/openjml-updatesite. The plug-in works with the Eclipse Neon.2 and later releases. After installation and restarting, you should see a 'JML' entry in the top menu bar.

The plug-in also needs SMT solvers as described above, for static checking.

Before performing static checking with the plug-in, you need to open the OpenJML Solvers preference page, set a default prover (e.g., z3_4_3), and enter the absolute path on your system to the prover executable.

If you have a directory tree of code to which you want to apply OpenJML, it is most convenient to import that code as an Eclipse Project:

SMT provers

In general, OpenJML can use any SMT-LIBv2-compliant solver, but since tools vary in their SMT-compliance and their support for various logics, adapter code is often needed. OpenJML has been tested with

THESE LINKS NEED UPDATING