Ghost Variable Exercises:

Ghost Variable Tutorial

Question 1

Suppose we want to implement integer pairs in such a way that the method lesserValue, which should return the element of the pair that is the least of the two integers, will be very efficient, and we are willing to trade a bit of extra space in the integer pairs for that efficiency. Then it might make sense to precompute the lesser of the two integers in the constructor, and to use ghost fields to remember which was intended to be the first field and the second field. This is the idea behind the following class. The exercise is to complete the decaration of the class by adding declarations of (public) ghost fields first and second, which remember which was the first and second argument to the constructor, and by setting those ghost fields to the appropriate values in the constructor. Then ensure that the entire class verifies using OpenJML.

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

    private /*@ spec_public @*/ final int lesser, greater;
    private /*@ spec_public @*/ final boolean increasing;

    // ADD DECLARATIONS OF GHOST FIELDS first AND second;

    //@ public invariant lesser <= greater;
    //@ public invariant lesser <= first && lesser <= second;
    // the following is a "representation invariant"
    //@ public invariant increasing ==> (first == lesser && second == greater);
    //@ public invariant !increasing ==> (second == lesser && first == greater);

    //@ ensures first == fv && second == sv;
    public IntPair(int fv, int sv) {
        // ADD SET STATEMENT FOR GHOST FIELD first
        // ADD SET STATEMENT FOR GHOST FIELD second
        increasing = (fv <= sv);
        if (increasing) {
            lesser = fv;
            greater = sv;
        } else {
            lesser = sv;
            greater = fv;
        }
   }

    //@ ensures \result <= first && \result <= second;
    //@ spec_pure
    public int lesserValue() {
        return lesser;
    }

    //@ ensures \result == first;
    //@ spec_pure
    public int firstElem() {
        return (increasing ? lesser : greater);
    }
}

Question 2 (Advanced)

In the class IntPair, the fields lesser, greater, and increasing are all declared as spec_public. See if you can eliminate all uses of spec_public in a version of IntPair by using model fields and private represents clauses, while declaring the fields lesser, greater, and increasing to all be just private (and not spec_public). Hint: you will need to use invariants, but all the invariants can be public.

Learning Objectives:

  • Understand how to use ghost fields and computations in specifications
  • Understand when to use ghost fields and computations.

Answer Key

Resources