Temporal logic for interface invariants

Question

I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available functions of the interface.

For example, suppose we have a simple interface (Java style) Sum:

interface Sum {
    public void add (int a);
    public int getSum();
}

I want to express in an invariant that getSum returns the summation of a in all calls to add(a), without using any data representation of this sum.

The only way I can think of doing this is by using some form of temporal logic. Is there any literature on this subject available I can read? Any pointers would be much appreciated.

Answer 1

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.

Answer 2

Whatever you do, your specification will turn out to have internal state reflecting the accumulator inside your object. For a class this simple, the specification won't be any simpler than the implementation. The point is that for much more complex cases the specification is simpler. Consider a dictionary, where you add data under a key and must be able to retrieve it later. Your specification can very well be the equivalent of a linear array of key/value pairs, and the search a simple linear search. Your implementation would perhaps be a scheme based on hashing or balanced binary trees. The specification is easy to reason with, you prove your implementation behaves the same as the specification, and you are set. Tomorrow you rip out the implementation, and replace it by some fancier structure, prove again that it complies with the specification. No changes elsewhere.

Specifications are essentially writing the same program again in another (hopefully easier to handle) programming language, probably foregoing any performance considerations, and reasoning that both programs do the same. The specification languages up to date have turned out much harder to use than the regular programming languages (and specifications can have bugs too...), and the proof that they behave the same isn't for the faint of heart. And if I come up with an idea of how my program should behave, and program that, it stands to reason that the specification and the final program will share the same misconceptions and missed corner cases. There have been spectacular failures of the "program verification" movement. Look at Berry's "Academic Legitimacy of the Software Engineering Discipline" (CMU/SEI-92-TR-34) for an example of a program of a couple dozen lines, written and "proved correct", then fixed and again verified for publication in academic journals by some of the maximal experts in the area several times, and which was wrong each round.