JML Logo

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

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

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

Execution

To execute OpenJML (command-line version), you need

  • An appropriate Java VM: Java 8
  • 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 $OJ
  • 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 $OJ/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". If you have customized your environment by putting the solver path in the openjml.properties file, then the -exec option and its argument may be omitted.


java -jar $OJ/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

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 $OJ/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). (Use a colon instead of a semicolon in the classpath on Linux and MacOS systems.)


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

The following output is produced:

B.java:9: JML An item is assigned that is not in the assignable statement
    k = i;
      ^
B.java:6: Associated declaration
  //@ modifies j;
      ^
B.java:8: JML postcondition is false
  public static void setj(int i) {
                     ^
B.java:7: Associated declaration
  //@ ensures j == i;
      ^
B.java:14: JML postcondition is false
    setj(3);
        ^
B.java:7: Associated declaration
  //@ ensures j == i;
      ^
B.java:13: JML postcondition is false
  public static void main(String[] args) {
                     ^
B.java:12: Associated declaration
  //@ ensures j == 1;
      ^

Here you see a postcondition failure reported both by setj, which checks the postconditions on exit, and by main, which checks the postconditions of methods it calls when they return. In addition, the postcondition of main fails when main itself exits.