OpenJML User Guide and Reference

OpenJML Installation and Execution

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

as a command-line tool to do type-checking, static checking or runtime checking,
as an Eclipse plug-in to perform those tasks, and
programmatically from a user's Java program

Installation
Execution
OpenJML in Eclipse

Installation

To install the command-line tool, complete these steps: [TBD - revise the discussion of SMT solvers ]

download the zip file or the tar.gz file. Then select (creating if necessary) a folder of your choice to hold the installation, cd to that directory, and either
- unzip the .zip file: gunzip openjml.zip
- or, untar the tar.gz file: tar -xvfz openjml.tar.gz
For static checking, you will need an SMT solver. Make a choice from the list below, and install it according to its instructions.

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 Kepler SR2 and Luna 4.4.0ff releases; most functionality may work with the Juno release (Eclipse 4.2.2ff), but support for Juno is deprecated..

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 (yices2 or z3_4_3), and enter the absolute path on your system to the prover executable.

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

Z3 (version 4.3) on Windows and Mac (not quite working yet on Linux)
CVC4 (version 1.2) on Windows
Yices (version 2.1) on Windows or Mac OSX
(Linux platforms may well work but have not been tested.)

Execution

To execute OpenJML, you need

An appropriate Java VM: Java 7
A copy of the OpenJML release. The release contains the openjml.jar, jmlspecs.jar, and jmlruntime.jar files. The release may be installed anywhere you like. In the examples below, the (absolute path or path relative to the current working directory to the) installation directory is indicated by $INSTALL
For static checking, an appropriate SMT solver.

There are a few important topics for the user to know; these are discussed at the indicated links:

Type-checking

The OpenJML tool operates like a Java compiler, on a set of files. For example, the command


java -jar $INSTALL/openjml.jar -no-purityCheck A.java

will type-check the Java and JML in the A.java file and any classes on which it depends. Include the full absolute or relative path to the openjml.jar file as needed. (The -noPurityCheck option suppresses many warnings about the use of non-pure functions, since the JDK libraries are not yet populated with appropriate pure annotations.)

For example, put the following text in a file named A.java and execute the command above.

public class A {

  //@ ensures \result == true;
  public void m() {}

}

The following output is obtained:

A.java:3: A \result expression may not be used in the specification of a method that returns void
  //@ ensures \result == true;
               ^
1 error

Static checking

To perform static checking of the JML specifications you will need an SMT solver to determine logical satisfiability. See the installation instructions and the list of provers above and select one or more to install on your system.

To run the static checker, use a command-line like the following, substituting the path to the (in this case Z3) executable in your system. If you are using yices, substitute "yices2" for "z3_4_3".


java -jar $INSTALL/openjml.jar -esc -prover z3_4_3 -exec path-to-executable -no-purityCheck B.java

For example, place the following text in the file B.java and execute the command above.

public class B {

  static int j,k;

  //@ requires i >= 0;
  //@ modifies j;
  //@ ensures j == i;
  public static void setj(int i) {
    k = i;
  }

  //@ ensures j == 1;
  public static void main(String[] args) {
    setj(3);
  }

}

The following output is produced:

B.java:9: warning: The prover cannot establish an assertion (Assignable) in method setj
    k = i;
      ^
B.java:6: warning: Associated declaration
  //@ modifies j;
      ^
B.java:13: warning: The prover cannot establish an assertion (Postcondition) in method main
  public static void main(String[] args) {
                     ^
B.java:12: warning: Associated declaration
  //@ ensures j == 1;
      ^
4 warnings

The first two messages point out that the specification of the method setj states that the field j (and nothing else) is modified by the method, but the method actually modifies k.
The second pair of messages points out that the call of setj in method main does not satisfy the postcondition; the "Associated declaration" warning that follows indicates the violated postcondition.

Runtime assertion checking

To compile the JML specifications in the given files and in any files that they reference as assertions to be checked at runtime, use the -rac option:


java -jar $INSTALL/openjml.jar -rac -noPurityCheck B.java

Then execute this command (the jmlruntime.jar is part of the OpenJML installation -- include the full path to that library as needed)


java -classpath ".;$INSTALL/jmlruntime.jar" B