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.

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: