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

There exists many ways of describing a specification in JML, and some ways can be more precise than others. Therefore, the solutions presented here are only one among a variety of possible solutions.

1 Specifying Methods Behavior

In this solution, one warning remain about a possible arithmetic overflow in nextFib, and indeed it is possible that this function results in an arithmetic overflow. Note that factorial could also result in an overflow, but this is not detected because OpenJML is not complete: it may miss potential errors.

public class SomeMath {
  // Divides two integers
  //@ requires y != 0;
  //@ ensures \result == x / y;
  public static /*@ pure */ int divide(int x, int y) {
    return x / y;
  }

  // Get the sign of a number
  //@ ensures (x == 0) ==> \result == 0;
  //@ ensures (x > 0) ==> \result == 1;
  //@ ensures (x < 0) ==> \result == -1;
  public static /*@ pure */ 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
  //@ ensures x % \result == 0;
  //@ ensures y % \result == 0;
  public static /*@ pure */ 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
  //@ requires x >= 0;
  //@ ensures \result >= 0;
  public static /*@ pure */ 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;

  //@ assignable a, b;
  //@ requires x > 0;
  //@ ensures a * b == x;
  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 = 0;
  public static int y = 1;
  //@ assignable x, y;
  //@ requires x > 0;
  //@ requires y > 0;
  //@ ensures x == \old(y);
  //@ ensures y == \old(x) + \old(y);
  //@ ensures \result == y;
  public static int nextFib() {
    int tmp = y;
    y = x+y;
    x = tmp;
    return y;
  }
}

2 Specifying Classes Behavior

2.1 Positive.java

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;
  //@ requires x >= 0;
  //@ ensures n == x;
  public void set(int x) {
    this.n = x;
  }
}

2.2 Account.java

public class Account {
  //@ public invariant balance >= 0;
  private /*@ spec_public */ int balance;

  //@ assignable balance;
  //@ ensures balance == 0;
  public Account() {
    this.balance = 0;
  }

  //@ assignable balance;
  //@ requires amount > 0;
  //@ ensures balance == \old(balance) + amount;
  public void deposit(int amount) {
    this.balance = this.balance + amount;
  }

  //@ assignable balance;
  //@ requires amount > 0;
  //@ ensures \old(balance) >= amount && balance == \old(balance)-amount;
  //@ signals(RuntimeException e) \old(balance) < amount && balance == \old(balance);
  public void withdraw(int amount) throws RuntimeException {
    if (this.balance < amount) throw new RuntimeException();
    this.balance = balance - amount;
  }
}

2.3 BoundedStack.java

public  class BoundedStack {
  //@ public invariant size >= 0;
  //@ public invariant size <= elems.length;
  private /*@ spec_public */ /*@ non_null */ int[] elems;
  private /*@ spec_public */ int size = 0;

  //@ assignable elems;
  //@ requires n > 0;
  //@ ensures elems.length == n;
  public BoundedStack(int n) {
    elems = new int[n];
  }

  //@ assignable size, elems[size];
  //@ requires size < elems.length - 1;
  //@ ensures size == \old(size) + 1;
  //@ ensures elems[size-1] == x;
  public void push(int x) {
    elems[size] = x;
    size++;
  }

  //@ assignable size, elems[size];
  //@ requires size > 0;
  //@ ensures size == \old(size) - 1;
  //@ ensures elems[size] == 0;
  public void pop() {
    size--;
    elems[size] = 0;
  }

  //@ requires size > 0;
  //@ ensures \result == elems[size-1];
  public /*@ pure */ int top() {
    return elems[size-1];
  }
}