World's most popular travel blog for travel bloggers.

[Answers] Temporal logic for interface invariants

, , No Comments
Problem Detail: 

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.

Asked By : user1838636

Answered By : D.W.

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.

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback