Research Topics in Software Quality – Session 8: Statically Verifying JML Annotations with OpenJML

OpenJML is a tool that can statically verify specifications of Java programs written in JML. We will use it to verify specifications of Java method and Java classes.

1 Installing OpenJML

This might not work on Linux and it is preferred to follow this exercise session on Windows. OpenJML does not work with Java 8 and it is therefore recommended to use it with Java 7.

  1. Get OpenJML from http://jmlspecs.sourceforge.net/openjml.tar.gz and decompress the file.
  2. Get the Z3 SMT solver from http://z3.codeplex.com/releases and decompress the file.

2 Performing Extended Static Checking (ESC) with OpenJML

To perform extended static checking of specification on a Java file that contains JML annotations, use the following command: 

$ java -jar openjml.jar -esc -prover z3_4_3 -exec z3-4.3.3.61c59fb4bf3c-x64-ubuntu-14.04/bin/z3 -noPurityCheck Foo.java

3 Specifying Methods Behavior

3.1 Format of specification

JML specifications are written in comments starting with: 

//@ ...

or, for multiple-line specifications: 

/*@ ...
  @ ...
  @*/

3.2 Assertions and assumptions

Assertions and assumptions can be made anywhere with the assert and assume keywords: 

//@ assert n != 0;
int x = m/n;
//@ assume i == m/n;

3.3 Method contracts

Specifications for method can be seen as contracts: what should be true when calling this function, and what will be true when this function returns. They can be defined using the keywords requires (pre-condition) and ensures (post-condition). The \result keywords represents the value returned by the function 

//@ requires x >= 0;
//@ ensures \result >= 0;
public static int isqrt(int x) {
  return (int) Math.sqrt(x);
}

3.4 Sort example

The contract for a sort method could be the following: 

/*@ requires a != null;
  @ ensures (\forall int i; 0 <= i && i < a.length-1; a[i] <= a[i+1]);
  @*/
public void sort(int a[]);

Specifications can any side effect free Java code, and support the following constructs:

  • \forall type variable; pre; post to represent the universal quantifier:

\[ \forall variable \in type : pre \Rightarrow post \]

  • \exists type variable; pre; post to represent the existential quantifier:

\[ \exists variable \in type : pre \land post \]

  • \old(expression) to represent the value of an expression before entering the function

3.5 Side effects

A method specification can declare non-local variables which can be modified by a method with the assignable keyword: 

public static int i = 0, j = 0;
//@ assignable i, j;
public static void foo() {
  i = j;
  j = 0;
}

Special keywords can be used to denote variables: \everything (used by default), and \nothing.

3.6 Pure functions

A Java method can be declared as pure, meaning that is has no side effect and returns the same output given the same input. Pure functions can then be used in specifications: 

public static /*@ pure */ int sign(int x) {
  if (x == 0)
    return 0;
  else if (x > 0)
    return 1;
  else
    return -1;
}

//@ ensures sign(\result) >= 0;
public static int abs(int x) {
  if (x >= 0)
    return x;
  else
    return -x;
}

3.7 Exceptions

A method specification can declare the conditions under which a function will declare exceptions: 

//@ ensures \result == x;
//@ signals(RuntimeException e) x < 0;
static int foo(int x) {
  if (x < 0) throw new RuntimeException();
  return x;
}

3.8 Multiple cases

A function may return different results depending on the values of its argument. This can be encoded in the specification using the also keyword. 

//@   requires x == 0;
//@   ensures \result = true;
//@ also
//@   requires x != 0;
//@   ensures \result = false;
public static bool isZero(int x) {
  return x == 0;
}

This can also be encoded using the implication connective: 

//@ ensures (x == 0) ==> \result = true;
//@ ensures (x != 0) ==> \result = false;
public static bool isZero(int x) {
  return x == 0;
}

3.9 Default method specification

A method with no declared specification has the following implicit specification: 

//@ requires true;
//@ assignable \everything;
//@ ensures true;
//@ signals(Exception e) true;

3.10 Exercises

Provide precise JML specifications for the following programs, and verify them with OpenJML: 

public class SomeMath {
  // Divides two integers
  public static int divide(int x, int y) {
    return x / y;
  }

  // Get the sign of a number
  public static int sign(int x) {
    if (x == 0) {
      return 0;
    } else if (x > 0) {
      return 1;
    } else {
      return -1;
    }
  }

  // Compute the greatest common divisor of x and y
  public static int gcd(int x, int y) {
    while (y > 0) {
       int tmp = x % y;
       x = y;
       y = tmp;
    }
    return x;
  }

  // Compute the factorial of a number
  public static int factorial(int x) {
    int result = 1;
    for (int i = 0; i <= x; i++) {
      result *= i;
    }
    return result;
  }

  // Factor a number into two of its divisors (very naive implementation)
  // Stores the result in class variables a and b
  public static int a, b;
  public static void factor(int x) {
    for (int i = 2; i <= x; i++) {
      if (x % i == 0) {
        a = i;
        b = x / i;
      }
    }
  }

  // Computes the number of the Fibonacci sequence, using an internal state
  public static int x = 1;
  public static int y = 1;
  public static int nextFib() {
    int tmp = y;
    y = x+y;
    x = tmp;
    return y;
  }
}

4 Specifying Classes Behavior

4.1 Class Invariants

Class invariants are formulas that are true before and after each method call. They can be specified in a class definition with the invariant keyword.

4.2 Visibility

In general it is recommended to distinguish the public specification of a class (implementation-independent) and its private specification (implementation-dependent), but it might not be possible to establish specifications without some variable representing the internal state of the class. To avoid that, it is advised to use model variables. In this exercise session however, we will write everything in the specification as public, in order to focus on the specification themselves.

4.3 Example

Below is an example of a simple class with a private variable that is public in the specification, and a public invariant on that variable. The given specification is incomplete. 

public class Positive {
  //@ public invariant n >= 0;
  private /*@ spec_public */ int n;

  //@ ensures n == 0;
  public Positive() {
    this.n = 0;
  }

  //@ ensures \result == n;
  public int get() {
    return this.n;
  }

  //@ assignable n;
  //@ ensures n == \old(n)+1;
  public void inc() {
    this.n++;
  }

  //@ assignable n;
  //@ ensures n == x;
  public void set(int x) {
    this.n = x;
  }
}

We can verify that the specification is indeed incomplete by running OpenJML on this class: 

$ java -jar openjml.jar -esc -prover z3_4_3 -exec path/to/z3 Positive.java
[...]
Positive.java:23: warning: The prover cannot establish an assertion (InvariantExit: Positive.java:2: ) in method set
  public void set(int x) {
              ^
Positive.java:2: warning: Associated declaration: Positive.java:23:
  //@ public invariant n >= 0;
             ^

Exercise: fix the specification by adding the missing specification clause.

4.4 Exercise: Bank Account

The following programs implement a bank account with the following informal specification:

  1. a bank account has a current balance, initially set to zero,
  2. the balance of a bank account cannot go below zero
public class Account {
  private int balance;

  public Account() {
    this.balance = 0;
  }

  public void deposit(int amount) {
    this.balance = this.balance + amount;
  }

  public void withdraw(int amount) {
    if (this.balance < amount) throw new RuntimeException();
    this.balance = this.balance - amount;
  }
}

Write this specification formally as JML annotations in the following program, and verify it with OpenJML.

4.5 Exercise: Bounded Stack

Write the JML specification of the following program, and verify it with OpenJML. 

public  class BoundedStack {
  private int[] elems;
  private int size = 0;

  public BoundedStack(int n) {
    elems = new int[n];
  }

  public void push(int x) {
    elems[size] = x;
    size++;
  }

  public void pop() {
    size--;
    elems[size] = null;
  }

  public int top() {
    return elems[size-1];
  }
}

5 Further information

Most of this exercise session is inspired by:

  • Slides and exercise sessions of Jochen Hoenicke's Formal Methods for Java course1.
  • Slides on JML specifications by Wolfgang Schreiner2.

Footnotes:

1

http://swt.informatik.uni-freiburg.de/teaching/winter-term-2011-2012/fm4j

2

http://www.risc.jku.at/education/oldmoodle/file.php/35/04-jml1.pdf and http://www.risc.jku.at/education/oldmoodle/file.php/35/05-jml2.pdf

Last update: 2015-12-04T14:57:21+01:00