JML uses invariant clauses to specify properties of an object that should “always” hold. This lesson describes the straightforward uses of such invariants and also the complexities of what “always” means.

Since invariants are validity properties:

  • a method may assume that the invariants are true in its pre-state, and
  • a method must ensure that the invariants are still true (or true again) in its post-state, and
  • a constructor must ensure that the invariants are true in its post-state. Thus one can think of an invariant as being simultaneously a precondition and a postcondition on all methods. However, since an invariant is like a precondition, the \old notation cannot be used in an invariant.

Simple invariants

The basic idea of an invariant is this: an invariant describes a property that always holds of an object. Every method can assume the invariants hold and must preserve these invariants. Constructors create objects that satisfy invariants. In this sense, invariants enable induction on objects of the type, since constructors must establish them and methods must preserve them.

A few points to keep in mind:

  • Invariants can be declared static, in which case they can name and apply to static fields. However, such static invariants apply to all methods, which must preserve them.
  • An invariant that is not declared to be static is an instance invariant, and these only apply to non-static methods.
  • Most invariants are declared public. See the discussion below about visibility.

Here is a typical simple example:

// openjml --esc MyBox.java
public class MyBox {
  private /*@ spec_public @*/ int size;

  //@ public invariant size >= 0;

  //@ requires sz >= 0;
  public MyBox(int sz) {
    size = sz;
  }

  public void doit() {
    int[] ints = new int[size];
  }

  //@ assignable size;
  public void shrink() {   // ERROR: doesn't establish invariant on exit!
    size = size - 10;
  }

  //@ public normal_behavior
  //@   ensures \result == size;
  //@ spec_pure
  public int size() {
    return size;
  }

  //@ public normal_behavior
  //@   ensures \result == size;
  //@ spec_pure
  //@ helper    // does not assume or establish the invariant
  public int sizeH() {
    return size;
  }

  //@ public normal_behavior
  //@   assignable size;
  //@ helper // does not assume or establish the invariant
  final public void changeSizeH() {
      java.util.Random r = new java.util.Random();
      int sz = r.nextInt(-10,10);
      size = sz;
  }

  public static void test1(MyBox b) {
    //@ assert b.size() >= 0;
  }
  public static void test2(MyBox b) {
    //@ assert b.sizeH() >= 0; // OK because sizeH() is pure
  }
  public static void test3(MyBox b) {
    //@ check b.size >= 0;
    b.changeSizeH();
    //@ check b.sizeH() == b.size;
    //@ check b.sizeH() >= 0; // ERROR: sizeH may not establish the invariant!
    b.size = 0;
  }
  public static void test4(MyBox b) {
    b.changeSizeH();
    //@ assert b.size() >= 0; // ERROR: invariants may not hold, so size() can't be called!
    b.size = 0;
  }
}

This example shows part of a simple class that has a size field. The specification records in its invariant clause that this size is always to be a non-negative integer. So the constructor guarantees (using a precondition) that size is non-negative when a MyBox is created. In doit(), size is used to create an array. The call of doit() can assume that the invariants of this hold at the beginning of the call; consequently it does not need to check that size is non-negative before using its value as the length of the new array.

On the other hand, shrink() is intended to make the MyBox smaller by reducing its size by 10. It correctly specifies that size is assignable. However, a verification attempt reports the following:

MyBox.java:17: verify: The prover cannot establish an assertion (InvariantExit: MyBox.java:5:) in method shrink
  public void shrink() {   // ERROR: doesn't establish invariant on exit!
              ^
MyBox.java:5: verify: Associated declaration: MyBox.java:17:
  //@ public invariant size >= 0;
             ^
MyBox.java:55: verify: The prover cannot establish an assertion (Assert) in method test3
    //@ check b.sizeH() >= 0; // ERROR: sizeH may not establish the invariant!
        ^
MyBox.java:60: verify: The prover cannot establish an assertion (InvariantEntrance: MyBox.java:5:) in method test4: (Caller: MyBox.test4(MyBox), Callee: MyBox.size())
    //@ assert b.size() >= 0; // ERROR: invariants may not hold, so size() can't be called!
                     ^
MyBox.java:5: verify: Associated declaration: MyBox.java:60:
  //@ public invariant size >= 0;
             ^
5 verification failures

Here InvariantExit means that on exit from the method, the invariant cannot be proven — which is clearly the case if the MyBox has a size less than 10 in the pre-state of the shrink() method.

helper methods

Sometimes it is useful or simpler if a method does not need to assume or ensure the invariants. In such a case, the method can be declared a helper method. This is the difference between size() and sizeH() in the code listing above.

size() is a conventional non-helper getter method. It assumes the invariant holds and returns the value of size. A client routine, such as test1(), can prove that mybox.size() >= 0 after creating a MyBox object.

sizeH() on the other hand is declared helper. It does not assume that size is non-negative. That does not matter here, but it would, for example if doit() were declared helper; in that case doit() would need a precondition that required size >= 0. sizeH() verifies OK, but when one uses it, one cannot be assured that the value of mybox.sizeH() is non-negative. Method test2() proves OK because, although sizeH() does not establish the invariant, it is spec_pure so it does not change size, and consequently it is provable that the invariant still holds on exit from test2(). In test3() on the other hand, the program state has been changed by helper method changeSizeH to something that may not satisfy the invariant. It is OK to call sizeH because it is helper and does not require the invariant. But then we don’t know that the value of sizeH() satisfies the invariant either.

If, as in test4(), we call size() instead of sizeH(), we find that there is a verification error because size() expects the invariants to hold when in fact they may not.

The cost of not having to have the invariants true on entrance to a method is that they may not be true on entering or exiting the method, though one can always add them into the pre- or postconditions in the method’s specification.

Visibility of invariants

  • Invariants have a visibility (public, private, etc.). Almost always, public is the appropriate modifier to use. Invariants with visibility other than public only apply where they can be “seen”, just like the modifiers when used for methods (and their specification cases).
  • Invariants cannot use fields or methods with a visibility more constrained than their own. Consequently, as in this case, a private field will need a spec_public declaration. See the lesson on Visibility for more on this topic.

Invariants when calling methods

Aside from helper methods, all other methods assume that their invariants are true in their pre-state. Thus when a method is called, the caller is responsible to be sure that the callee’s invariants are true before invoking the callee, just as the caller has to be sure that the callee’s preconditions hold before invoking the callee. (This is what causes the verification failure of test4() in the class MyBox above.) Thus the callee generally expects that, in addition to the invariants of its own class, the invariants of all of its formal parameters also hold.

In JML verification of a method in a class does not automatically assume the invariants of other classes, so if those invariants are needed for verification, they should be specified in the method’s preconditions. This is especially true when another class’s state is accessed without calling its methods (e.g., when assigning to fields of another class). One can use the expression \invariant_for(E) to refer to the invariants of E. There is also an expression \static_invariant_for(T) that means the static invariant of a type T. See the “JML Expressions” chapter of the JML Reference Manual for details on these.

To be sure that invariants hold whenever a method is called, each non-helper method must restore its invariants before calling another method. This is necessary when calling a method in the same class (including recursive calls), since the callee will immediately assume the invariant. For a call to a method in another class, the callee might call back to the original method with the broken invariant, leading to an invalid assumption of that invariant. Thus, JML requires that an object’s invariants be re-established before calling another method. This is shown in the following code snippet.

public class SomeClass {
  //@ public invariant ...

  public void m(SomeOtherClass o) {
    // some code that temporarily invalidates the invariant of SomeClass
    o.dosomething(this);
    // code that restores the invariant of SomeClass
  }
}

When OpenJML attempts to verify the method SomeClass.m, it finds that the call o.dosomething could be made when the invariant (of SomeClass) is invalid. The problem is that o.dosomething might call a method of SomeClass on its argument (this), but that method would then be called in a state in which its assumed invariant does not hold. To prevent such situations, all invariants of this must be established before the call to o.dosomething. A general way around this restriction is to declare a method to be a helper method, and then any invariants needed for verification can be added to the method’s pre- and/or postconditions.

! Just which invariants are required to hold before a method call is a topic of research and discussion. OpenJML is experimenting with defaults that are both convenient and sound.

Exercises

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

Resources