It is sometimes helpful (for specification or verification) to include in a program various variables or computations that are intended only for specification or verification. In JML one can use a ghost field to, for example, keep track of information about an object class that the Java implementation does not track. Or, in the body of a method, one may want to record some value or perform some computation for the purpose of checking the Java implementation, but not have that variable or computation be part of the Java implementation or compiled into the Java class (and thus not be executed when running the code).

This can be particularly helpful if the ghost computation is easier to understand than some complicated (and hopefully faster) algorithm or data structure, especially when the ghost computation can be used to check the computation that the code performs at runtime.

JML provides ghost declarations and various JML-only statements for this purpose:

  • Field declarations can be modified with the ghost keyword and placed in a JML comment. Such fields are in scope for specifications but not in Java code.
  • The JML set statement permits assignments and computations that are only done in the specification (not in the code): 
    //@ ghost int i = x; // x may be a Java variable
//@ set i = i + 10; // a ghost computation

    set statements may also include pure method calls.

The values of ghost variables may then be used in subsequent JML assert (and assume) statements. These ghost variables and ghost computations can be used to prove that some step taken in algorithm or data structure design is justified. Alternatively, they may be used to point out to the reader some properties of the code written (such as its time efficiency or the equivalence of some sophisticated data structure to a straightforward one), without incurring a (time or space) penalty at runtime. Furthermore, ghost variables may be used to make stating assertions (or assumptions) easier.

An example can be seen in the following class declaration.

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

    private /*@ spec_public @*/ int a = -1;
    private /*@ spec_public @*/ int b = -1;
    //@ public ghost int mean;

    // once the object exists the values of a and b are non-negative
    //@ public invariant (0 <= a && 0 <= b);
    //@ public invariant a+b <= Integer.MAX_VALUE;
    //@ public invariant (mean == (a+b)/2);

    //@ requires 0 <= av && 0 <= bv && av+bv <= Integer.MAX_VALUE;
    //@ ensures a == av && b == bv;
    //@ ensures mean == (a+b)/2;
    public T_Ghost(int av, int bv) {
        a = av;
        b = bv;
        //@ set mean = (a+b)/2;
    }

    //@ ensures \result == mean;
    public int average() {
        return (a+b)/2;
    }
}

In the above example, the ghost field mean is not present in the implementation, so it does not use any space at runtime (except during runtime assertion checking). It is used in the postcondition of the average() method to explain that what is returned is the average of the values of the fields a and b.

JML also has model fields and represents specification that can be used to help specify classes and interfaces. These are also specification-only constructs. (See the section on model fields and datagroups.) For example, the ghost field mean in the above example could have been declared as a model field with a represents clause giving its value as the average of a and b.

Exercises

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

Resources

+T_Ghost file