JML Logo

Running OpenJML (Command-line version)

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.

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

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 A.java

will type-check the Java and JML in the A.java file and any classes on which A.java depends. Include the full absolute or relative path to the openjml.jar file as needed.

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 run the static checker, use a command-line like the following.


java -jar $OJ/openjml.jar -esc B.java

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

public class B {

  static /*@ spec_public*/ int j,k;

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

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

}

The following output is produced; the various pairs of warnings can be output in any order:

B.java:16: warning: The prover cannot establish an assertion (Postcondition: B.java:13: ) in method main
    return;
    ^
B.java:13: warning: Associated declaration: B.java:16: 
  //@ ensures j == 1;
      ^
B.java:10: warning: The prover cannot establish an assertion (Postcondition: B.java:7: ) in method setj
    return;
    ^
B.java:7: warning: Associated declaration: B.java:10: 
  //@ ensures j == i;
      ^
B.java:9: warning: The prover cannot establish an assertion (Assignable: B.java:6: ) in method setj:  k
    k = i;
      ^
B.java:6: warning: Associated declaration: B.java:9: 
  //@ modifies j;
      ^
6 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 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:8: JML postcondition is false
  public static void setj(int i) {
                     ^
B.java:7: Associated declaration: B.java:8: 
  //@ ensures j == i;
      ^
B.java:14: JML postcondition is false
  public static void main(String[] args) {
                     ^
B.java:13: Associated declaration: B.java:14: 
  //@ 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.