4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ What are temporal aspects you think you need to model? $\endgroup$ – Raphael Apr 12 '13 at 7:15
  • $\begingroup$ Well, in an ideal world I would need access to all parameters and return values off all method calls made in the past. I think it may be possible to reduce this a bit by doing some form of "temporal recursion", but I think everything will get more complicated by doing this. $\endgroup$ – user1838636 Apr 12 '13 at 10:21
  • $\begingroup$ I think you can specify directly that any finite chain of add results in the correct return value of getSum. That the value does not change in between add calls might be more intricate. $\endgroup$ – Raphael Apr 12 '13 at 10:57
  • $\begingroup$ How would you specify this? $\endgroup$ – user1838636 Apr 12 '13 at 13:08
  • $\begingroup$ Depends on the Syntax/logic you allow. $\endgroup$ – Raphael Apr 12 '13 at 13:17
2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Well, given that you do not get to use any temporal logic, you would indeed need some internal accumulator in the specification. I want, however, to do it without any internal state, and in that case temporal logic seems to be a solution. I don't know, however, if there has been any research in this area. A specifiction may indeed contain bugs, but you can use it to make sure different implementations behave the same. $\endgroup$ – user1838636 Apr 12 '13 at 12:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.