Assert Statements

A JML assert statement states a condition that is expected to hold during execution where the statement appears. Such statements are not part of a method’s interface specification, but they can help debug the code of a method or show where a proof is not working. For example, an assert statement can provide a lemma that aids verification.

An assert statement is simple: in a JML comment, it is just the keyword assert followed by a predicate and terminated with a semicolon, as in the following example.

// openjml --esc T_assert1.java

public class T_assert1 {

  public void example(int i) {
    int neg;
    if (i > 0) {
      neg = -i;
    } else {
      neg = i;
    }
    //@ assert neg <= 0;
  }
}

The above example verifies with OpenJML, but the following variation does not:

// openjml --esc T_assert2.java

public class T_assert2 {

  public void example(int i) {
    int neg;
    if (i > 0) {
      neg = -i;
    } else {
      neg = i;
    }
    //@ assert neg < 0;  // ERROR: may be false!
  }
}

Indeed, running ESC on T_assert2.java produces the following.

T_assert2.java:12: verify: The prover cannot establish an assertion (Assert) in method example
    //@ assert neg < 0;  // ERROR: may be false!
        ^
1 verification failure

This verification error occurs because if i is 0, then neg is 0 so the assertion will fail. In this second example, which is at fault: the code or the assert statement? The answer depends on what the intent of the method is: should neg be a negative number or a non-positive number? The OpenJML tool can only identify the discrepancy between the code and the specification, giving the software and/or specification writer the opportunity to consider the problem and make an appropriate correction.

Java Assert Statements

Java has its own assert statement. However, by default, the Java assert statements are ignored at runtime, unless explicitly enabled. When enabled (using the virtual machine’s -ea or -esa runtime option) a Java program will throw an AssertionError if the predicate in the Java assert statement is false (at runtime).

During ESC, OpenJML verifies Java assert statements in the same way that it verifies JML assert statements; it issues a verification error if it cannot prove the designated predicate is always true. So the following example, like the example above,

// openjml --esc T_assert3.java

public class T_assert3 {

  public void example(int i) {
    int neg;
    if (i > 0) {
      neg = -i;
    } else {
      neg = i;
    }
    assert neg < 0; // A Java assert (interpreted by JML) // ERROR: may be false!
  }
}

produces similar output:

T_assert3.java:12: verify: The prover cannot establish an assertion (Assert) in method example
    assert neg < 0; // A Java assert (interpreted by JML) // ERROR: may be false!
    ^
1 verification failure

Check Statements

The check statement (e.g., check neg < 0;) is similar to an assert statement in that it also tests whether the given predicate is always true. However, the two statements differ in their effect on the subsequent logic of the program:

  • A check statement tests the predicate but makes no assumption about whether the predicate is subsequently true. A check statement essentially says, “just check whether the given predicate is true here”.
  • An assert predicate tests the predicate and then assumes that it is subsequently true. An assert statement essentially says, “this predicate is supposed to be true, so test it, and assume it to be true for analyzing subsequent code.”

For example,

// openjml --esc T_assert4.java

public class T_assert4 {
  public int f;

  public void example(/*@ nullable */ T_assert4 t) {
    //@ check t != null; // check ERROR: because not necessarily so!
    int k = t.f; // ERROR: because t might be null!
  }

  public void example2(/*@ nullable */ T_assert4 t) {
    //@ assert t != null; // assert ERROR: because not necessarily so
                          // but subsequently assumes it is true!
    int k = t.f; // assumed to be true, so no error given here
  }

}

produces this output:

T_assert4.java:8: verify: The prover cannot establish an assertion (PossiblyNullDeReference) in method example
    int k = t.f; // ERROR: because t might be null!
             ^
T_assert4.java:7: verify: The prover cannot establish an assertion (Assert) in method example
    //@ check t != null; // check ERROR: because not necessarily so!
        ^
T_assert4.java:12: verify: The prover cannot establish an assertion (Assert) in method example2
    //@ assert t != null; // assert ERROR: because not necessarily so
        ^
3 verification failures

This explanation points to a potentially confusing point about assert statements. If the given predicate is always false, then the implicit assumption, after the assert statement, is that the predicate is true, and that allows the following code to verify vacuously, since there is no pre-state for the following statement satisfying the asserted predicate. A check statement should be used to find subsequent errors that result from such predicates (i.e., those that might always be false).

Exercises

Follow the link in the above heading to work on the exercises on this topic.

Resources