public class CounterGhost { //@ public ghost int value; private int increments; //@ in value; private int decrements; //@ in value; //@ private invariant value == increments - decrements; //@ assignable value; //@ ensures value == 0; public CounterGhost() { increments = 0; decrements = 0; //@ set value = 0; } //@ assignable value; //@ ensures value == \old(value+1); public void increment() { increments = increments + 1; //@ set value = value + 1; } //@ assignable value; //@ ensures value == \old(value-1); public void decrement() { decrements = decrements + 1; //@ set value = value - 1; } //@ ensures \result == value; public /*@ pure @*/ int get() { return increments - decrements; } }