Runtime Assertion Checking (RAC): Compilation and Execution

A JML-annotated Java program can be compiled and executed like any Java program, but with the JML assertions checked at runtime. The JML assertions are only checked for the particular values of inputs, variables, etc. that occur during that particular run of the program, not for all possible inputs (as in static deductive verification). Furthermore not all JML constructs are executable; some will be ignored during compilation for RAC.

Compilation

The openjml tool when used with the -rac option compiles a Java program with runtime assertions added. In this mode openjml functions much like javac: it has the same Java command-line options (like -cp or --classpath), along with additional OpenJML options.

For example,

// openjml -rac T_Rac1.java
public class T_Rac1 {

  public static void main(String... args) {
    //@ assert args.length == 1;
  }
}

compiles with openjml -rac T_Rac1.java to produce a T_Rac1.class file.

Execution

The RAC-compiled Java program can then be executed in two ways: either using openjml-java or the standard installed java. If you are using openjml-java you do not need to have an installatino of Java itself.

openjml-java

openjml-java is a build of java produced and installed along with openjml. It functions like java except that it includes the runtime libraries needed for RAC. So to run the program compiled above one just executes

openjml-java -cp . T_Rac1

producing

T_Rac1.java:5: verify: JML assertion is false
    //@ assert args.length == 1;
        ^

If you run it with one command-line argument, then the assertion in the program is true and does not produce any error messages:

openjml-java -cp . T_Rac1 hi

java

If you have java (at least v. 17, as of 5 December 2021) installed on your system, you can use it to run the RAC-compiled program produced by openjml. You need to include in your classpath the JML runtime library, jmlruntime.jar, which is available in the OpenJML installation. If $OJ is the path to the installation folder containing openjml and jmlruntime.jar then you can run the RAC-compiled class file from above as

java -cp .:$OJ/jmlruntime.jar T_Rac1

producing

T_Rac1.java:5: verify: JML assertion is false
    //@ assert args.length == 1;
        ^