A JML assert statement states a condition that is expected to hold at a point within the body of a method. Such statements are not part of a method’s interface specification, but they can help (either staticly with ESC or at runtime with RAC) debug the execution of a method or, sometimes, provide a lemma that aids in the verification of the method body.

An assert statement is simple: in a JML comment, it is just the assert keyword 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;
  }
}

produces

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

because if i is 0, then neg is 0 and the assert fails. In this second example, which is at fault: the code or the assert statement? Well, that depends on what the intent of the method is: should neg be a negative number or a non-positive number? The verifier can only identify the discrepancy between the code and the specification, giving the software writer the opportunity to consider the problem and make an appropriate correction.

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

OpenJML will interpret a Java assert statement in the same way that it does a JML assert statement; it issues a verification error if it cannot prove the designated predicate true. So this 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 statement (but interpreted by JML)
  }
}

produces similar output:

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

Check statement

The check statement (e.g. check neg < 0;) is similar to the assert statement. It also effects a test of 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 or false. A check statement essentially says, please just check whether the given predicate is true or false.
  • 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 pleasae 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; // 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; // ERROR, because not necessarily so
                          // but subsequently assumes it is true
    int k = t.f; // OK
  }

}

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; // ERROR, because not necessarily so
        ^
T_assert4.java:12: verify: The prover cannot establish an assertion (Assert) in method example2
    //@ assert t != null; // 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 check, that it is true causes a complete halt to the symbolic execution – there is no pre-state that satisfies the assert/assume combination. A check would be better to be used in such cases.

Assert Statements Problem Set