Frame Conditions Exercises Key:

Frame Conditions Tutorial

Question 1

Adding a frame condition that says that maxValue can be assigned in the method determineMax() and one that says that xGretaterThanY() has no effects (or is spec_pure or pure), allows the program to be verified, as in the following. (Note that constructors cannot be spec_pure since they can only be called when constructing objects, hence the constructor below can only be pure.)

public class FrameCondEx1 {
    private /*@ spec_public @*/ int maxValue;
    private /*@ spec_public @*/ int x;
    private /*@ spec_public @*/ int y;

    //@ ensures x == xv && y == yv;
    //@ pure
    public FrameCondEx1(int xv, int yv) {
        x = xv;
        y = yv;
    }

    //@ assignable maxValue;
    //@ ensures x == maxValue || y == maxValue;
    //@ ensures x <= maxValue && y <= maxValue;
    public void determineMax() {
        boolean xgty = xGreaterThanY();
        if (xgty) {
            maxValue = x;
        } else {
            maxValue = y;
        }
    }

    //@ ensures \result <==> (x > y);
    //@ spec_pure
    public boolean xGreaterThanY() {
        return x > y;
    }

    public void test() {
        FrameCondEx1 fc12 = new FrameCondEx1(1,2);
        //@ assert fc12.x == 1;
        //@ assert fc12.y == 2;
        fc12.determineMax();
        //@ assert fc12.maxValue == 2;
        //@ assert fc12.x == 1;
        //@ assert fc12.y == 2;
    }
}

Explanation: The problem, as one can see by running ESC on the code in the exercise (which gives the following output)

FrameCondEx1.java:36: verify: The prover cannot establish an assertion (Assert) in method test
        //@ assert fc12.maxValue == 2;   // ERROR: may fail!
            ^
FrameCondEx1.java:37: verify: The prover cannot establish an assertion (Assert) in method test
        //@ assert fc12.x == 1;    // ERROR: may fail!
            ^
2 verification failures

is that the specification of determineMax() does not prevent that method from changing either x or y. So one should add to the specification of determineMax() the following frame condition.

    //@ assignable maxValue;

(or a synonym, such as assigns maxValue).

However, if one only makes that change, then call of xGreaterThanY() in determineMax also causes several verification errors, including the following.

FrameCondEx1.java:27: warning: Method xGreaterThanY() has 'assignable \everything', making its caller likely impossible to verify
    //@ ensures \result <==> (x > y);
        ^

The trouble is that the verification of the call to xGreaterThanY() assumes that it does not change the class’s fields. However, since JML does verification method by method, the specification of xGreaterThanY() needs to say that, thus the xGreaterThanY() method needs to be declared as assignable \nothing or pure (but we prefer spec_pure, see the discussion about using methods in specifications for why).

Question 2

The following is one rewriting that does verify.

public class Money {
    private /*@ spec_public @*/ int dollars, cents;

    //@ requires c < 100;
    //@ ensures dollars == d && cents == c;
    public Money(int d, int c) {
        dollars = d;
        cents = c;
    }

    //@ requires this != m;
    //@ requires cents < 100;
    //@ requires m.cents < 100;
    /*@ ensures \result <==> (this.dollars == m.dollars
      @                        && this.cents == m.cents); @*/
    public /*@ spec_pure @*/ boolean equals(Money m) {
        return this.dollars == m.dollars && this.cents == m.cents;
    }
        
    //@ requires dollars + cents/100 <= Integer.MAX_VALUE;
    //@ assignable dollars, cents;
    //@ ensures cents < 100;
    public void normalize() {
        if (cents >= 100) {
            dollars += cents/100;
            cents = cents % 100;
        }
    }
}

Explanation: The above solution adds a frame condition to the method normalize(), which limits the fields that can be changed to just the dollars and cents of the receiver (this); this change allows calls to normalize to be verified. However, since the equals method must remain spec_pure it cannot call normalize (on either the receiver or on m), as those calls may have effects. Thus its calls to the non-pure method normalize() must be removed. It therefore is sensible to change the specification of equals to require that the objects being compared are already normalized. (With this change, the precondition this != m is no longer needed for the equals method.) Instead of requiring both object to already be normalized, a better solution might be to enforce an invariant (that cents < 100 for all Money objects); see the tutorial section on invariants for more about this.

Resources: