A standard method is to use so-called ghost variables. A ghost variable is just like an ordinary variable, except it appears only in the specification (it isn't part of the program that actually executes). In other words, the ghost variable is not present in the original program; it is added by the spec. The preconditions, postconditions, and invariants are allowed to refer to the ghost variable.
Intuitively, a ghost variable allows you to maintain state about what methods have been invoked in the past; the specifications for those methods can update the ghost variable, thus remembering this information.
We can solve your specific challenge problem by adding a ghost variable totalSoFar
. Then, we add an appropriate specification for each method, like this:
interface Sum {
ghost int totalSoFar = 0;
/* postcondition: totalSoFar = old(totalSoFar) + a */
public void add (int a);
/* postcondition: returnvalue = totalSoFar */
public int getSum();
}
Notice how the postcondition for add()
updates the ghost variable, based upon the parameter passed to add()
. Similarly, the postcondition for getSum()
describes its return value in terms of the ghost variable.
This is the standard pattern: you use ghost variables to keep track of whatever state you need; for methods that modify this state, you write postconditions to update the state in the ghost variables; and for getters, you express their result in terms of the state of the ghost variables.
add
results in the correct return value ofgetSum
. That the value does not change in betweenadd
calls might be more intricate. $\endgroup$