In the current state of deductive verification technology it is essential that all loops have loop specifications.

A loop typically has the following steps:

  • some initialization code
  • a loop condition, which (when false) causes the control flow to exit the loop
  • a loop body
  • an update statement that typically moves a loop index variable to the next value
  • and then control returns to testing the loop condition

There are four aspects of a loop that may need to be specified:

  1. a constraint on the expected values of the loop index (including just before exiting the loop), given by a loop invariant (a JML maintaining specification),
  2. an inductive predicate that says what has been accomplished so far by the loop, given also by a loop invariant,
  3. a loop frame condition that says which memory locations are modified by any iteration of the loop body, and
  4. a termination condition (with an integer type, given by a JML decreases specification) that enables proving that the loop will terminate.

While the loop frame condition (point 3 above) is always needed, OpenJML will try to infer it when it can. (And OpenJML can do this for all of the examples that verify in this section.) However, it is better to specify the loop frame condition and have JML check it than to rely on OpenJML to infer the loop frame condition.

For loops

Here is a typical, simple for loop with specifications:

// openjml --no-show-summary --esc T_forloop.java
public class T_forloop {

  public void setToRamp(int[] a) {
    //@ maintaining 0 <= i <= a.length;
    //@ maintaining (\forall int k; 0 <= k < i; a[k] == k);
    //@ loop_writes i, a[*];
    //@ decreases a.length - i;
    for (int i = 0; i < a.length; i++) {
        a[i] = i;
    }
    //@ assert \forall int i; 0 <= i < a.length; a[i] == i;
  }
}

The loop has a loop index i that counts up from 0, exiting the loop when it reaches the length of the input array. On each iteration, the loop body sets the ith element of the array to the value of the index i.

  • The first loop invariant states what values the loop index will have. If the range is too small, then the desired property for the whole array will not be provable. If the range is too large, then OpenJML will attempt to check the loop body for these out of range values, likely reporting errors. Very importantly, the range must include the value the loop index will take on when it exits the loop. So in this case the range is 0 <= i <= a.length, not 0 <= i < a.length.
  • The second maintaining clause states what has been accomplished in i iterations, namely that each array element up to (but not yet including) i is initialized to the expected value. Such an invariant is typically a \forallexpression.
  • The third specification clause states which memory locations are modified by the loop body.
  • And the decreases specification states a quantity that must decrease on each iteration but will always be non-negative when the loop body is executed. If those conditions are satisfied (and the verifier checks them), then we know that the loop will eventually terminate.

It may help to understand what the verifier tries to prove about a loop. It tries to prove three things:

  • First, when control flow reaches the loop (after the loop initialization), the loop invariants must be true. In the example above, i is 0 at this point, so both maintaining clauses are true.
  • Second, it:
    • assumes it knows nothing about the memory locations in the loop frame condition (which includes the loop index)
    • it then assumes that the loop invariants hold
    • it also establishes that the value of the termination expression at the beginning of the loop body is non-negative
    • and then assumes that the loop condition is true
    • it then applies the actions of the loop body
    • it does the update step
    • the resulting state must satisfy the loop invariants again (this includes using the updated value of the loop index)
    • it verifies that the termination expression has decreased
  • Third, it assumes the first two steps above and that the loop condition is false, and then proves that the loop invariants still hold

In the example above, the second proof obligation assumes 0 <= i <= a.length and (\forall int k; 0 <= k < i; a[k] == k) and that the loop is on-going so (i < a.length), and then it applies a[i]=i and i++, and proves (\forall int k; 0 <= k < i_post; a[k]==k), where the value of i_post is the updated value of the variable i.

It also must prove that a.length-i is non-negative at the start of the loop body (when the loop will be entered, logically this means that the loop test i < a.length must imply the predicate a.length-i >= 0) and that after the loop index update that value is greater than the new value of the expression, namely a.length-i_post, where the value of i_post is the updated value of the variable i.

The third proof obligation assumes 0 <= i <= a.length and (\forall int k; 0 <= k < i; a[k] == k) and !(i < a.length); the loop invariants are still true, trivially and that they in turn imply the truth of the assert statement.

In this example, the loop_writes statement can be omitted and the code will still verify, because the loop is simple enough that JML can infer the value of the loop frame condition from the statements in the loop and its body.

For-each loops

Java also has a loop syntax that does not have any loop index. In that case, the built-in JML variable \count can be used — its value is the number of loop body executions so far. In the for loop above, it would have the same value as i.

Here is a typical for-each loop:

// openjml --esc T_foreach.java
public class T_foreach {

  //@ ensures \result == (\forall int i; 0 <= i < a.length; a[i] > 0);
  public boolean allPositive(int[] a) {
    //@ maintaining 0 <= \count <= a.length;
    //@ maintaining (\forall int k; 0 <= k < \count; a[k] > 0);
    //@ loop_writes \nothing;
    //@ decreases a.length - \count;
    for (int v: a) {
      if (v <= 0) return false;
    }
    return true;
  }
}

Note that the (second) loop invariant states that so far (up to array index \count) all array elements are positive. That is because at the beginning of any loop iteration, all elements seen have been positive. As soon as a non-positive element is seen, the loop exits prematurely, but the verifier can follow this control flow to prove that the postcondition is valid for either exit.

Note also the use of \count as a stand-in for a loop counter and the use of \nothing to say that nothing is modified in the loop body, other than \count, which is implicitly included as a modified variable by OpenJML.

While loops

A while loop generally follows the same pattern as a traditional for loop. Here we give another example that does not have an explicit loop index.

// openjml --esc T_whileloop.java
public class T_whileloop {

  //@ requires a.length % 2 == 0;
  void alternate(boolean[] a) {
    int k = 0;
    //@ maintaining 0 <= \count <= a.length/2;
    //@ maintaining k == 2*\count && (\forall int j; 0 <= j < k; a[j] == (j%2 == 0));
    //@ loop_writes k, a[*];
    //@ decreases a.length - \count;
    while (k < a.length) {
      a[k+1] = false;
      a[k] = true;
      k += 2;
    }
    //@ assert (\forall int i; 0 <= i < a.length; a[i] == (i%2 == 0));
  }
}

Do-while loops

Do-while loops can be tricky to specify because they do not follow the same update-at-the-start of a loop pattern. Also, the loop body is executed at least once, because the loop condition is not evaluated until the end of the loop body. Here is a simple example.

// openjml --esc T_dowhile.java
public class T_dowhile {

  //@ requires 20 < a.length;
  public void test(int[] a) {
    int i = 0;
    //@ maintaining i == \count && 0 <= i <= 10;
    //@ maintaining (\forall int k; 0 <= k < i; a[k] == 0);
    //@ loop_writes i, a[*];
    //@ decreases 10-i;
    do {
      a[i] = 0;
      ++i;
    } while (i < 10);
    //@ assert (\forall int k; 0 <= k < 10; a[k] == 0);
  }
}

Loop verification errors

The examples above all verify, but the following are some examples showing several kinds of verification errors that are produced by erroneous specifications.

Loop initialization error

In this example, the initial value of i does not satisfy the first loop invariant:

// openjml --no-show-summary --esc T_LoopInitError.java
public class T_LoopInitError {

  public void setToRamp(int[] a) {
    //@ maintaining 0 < i <= a.length;
    //@ maintaining (\forall int k; 0 <= k < i; a[k] == k);
    //@ loop_writes i, a[*];
    //@ decreases a.length -i;
    for (int i = 0; i < a.length; i++) {
        a[i] = i;
    }
    //@ assert (\forall int i; 0 <= i < a.length; a[i] == i);
  }
}

producing this output:

T_LoopInitError.java:5: verify: The prover cannot establish an assertion (LoopInvariantBeforeLoop) in method setToRamp
    //@ maintaining 0 < i <= a.length;
        ^
1 verification failure

Loop body error

In this example, a loop invariant cannot be proven after execution of the loop body. To help debug this problem, a show statement (see Inspecting Counterexamples) is included, which shows that the problem occurs when the loop index is one less than the array length. Indeed, in that case, when the loop index is incremented on the final loop iteration, its value will be the array length, and then the first loop invariant will not hold. Interestingly, there is also a loop initialization error. Why? Because if a.length is 0, then the initial value of i does not satisfy the first loop invariant.

// openjml --esc --solver-seed=42 T_LoopBodyError.java
public class T_LoopBodyError {

  public void setToRamp(int[] a) {
    //@ maintaining 0 <= i < a.length;
    //@ maintaining (\forall int k; 0 <= k < i; a[k] == k);
    //@ loop_writes i, a[*];
    //@ decreases a.length - i;
    for (int i = 0; i < a.length; i++) {
        a[i] = i;
        //@ show i, a.length;
    }
    //@ assert (\forall int i; 0 <= i < a.length; a[i] == i);
  }
}

produces

T_LoopBodyError.java:5: verify: The prover cannot establish an assertion (LoopInvariantBeforeLoop) in method setToRamp
    //@ maintaining 0 <= i < a.length;
        ^
T_LoopBodyError.java:11: verify: Show statement expression i has value 0
        //@ show i, a.length;
                 ^
T_LoopBodyError.java:11: verify: Show statement expression a.length has value 1
        //@ show i, a.length;
                    ^
T_LoopBodyError.java:5: verify: The prover cannot establish an assertion (LoopInvariant) in method setToRamp
    //@ maintaining 0 <= i < a.length;
        ^
4 verification failures

(The order of error messages and the specific values returned by show are not guaranteed.)

Loop decreases error

If the decreases expression does not decrease, one receives the error shown in this example:

// openjml --no-show-summary --esc T_LoopDecreasesError.java
public class T_LoopDecreasesError {

  public void setToRamp(int[] a) {
    //@ maintaining 0 <= i <= a.length;
    //@ maintaining (\forall int k; 0 <= k < i; a[k] == k);
    //@ loop_writes i, a[*];
    //@ decreases i;
    for (int i = 0; i < a.length; i++) {
        a[i] = i;
    }
    //@ assert (\forall int i; 0 <= i < a.length; a[i] == i);
  }
}

with the output

T_LoopDecreasesError.java:8: verify: The prover cannot establish an assertion (LoopDecreases) in method setToRamp
    //@ decreases i;
        ^
1 verification failure

Negative termination value

If the termination expression can be negative at the start of a loop, one gets this behavior:

// openjml --no-show-summary --esc T_LoopNegativeError.java
public class T_LoopNegativeError {

  public void setToRamp(int[] a) {
    //@ maintaining 0 <= i <= a.length;
    //@ maintaining (\forall int k; 0 <= k < i; a[k] == k);
    //@ loop_writes i, a[*];
    //@ decreases -i;
    for (int i = 0; i < a.length; i++) {
        a[i] = i;
    }
    //@ assert (\forall int i; 0 <= i < a.length; a[i] == i);
  }
}

which produces

T_LoopNegativeError.java:8: verify: The prover cannot establish an assertion (LoopDecreasesNonNegative) in method setToRamp
    //@ decreases -i;
        ^
1 verification failure

Loop conditions with side effects

Good programming style avoids loop conditions with side effects. Nevertheless, such constructs are legal Java. However, writing workable specifications for such programs is tricky, reflecting the fact that understanding and writing correct programs using conditions with side-effects is tricky.

Specifying Loops Problem Set