Jul 19, 2010 at 2:23 PM
Edited Jul 19, 2010 at 2:27 PM
in the code below, I use a call to a pure method in an object invariant. Spec# gives the following warnings:
Warnung 1 The call to A.get_a() requires target object to be peer valid C:\Users\hollas\Documents\Visual Studio 2008\Projects\test\test\Program.ssc 9 17 test
Warnung 2 Object invariant possibly does not hold: 0 <= get_a() C:\Users\hollas\Documents\Visual Studio 2008\Projects\test\test\Program.ssc 20 2 test
These warnings disappear when I replace the method call by the referenced variable. What is wrong?
invariant 0 <= get_a(); //_a
[Pure] public int get_a()
ensures 0 <= _a;
_a = 1;
[Rep] A a = new A();
invariant 0 <= a.get_a();
Jul 20, 2010 at 12:54 AM
As you are discovering, pure methods are trickier than one would expect (and, indeed, trickier than we would wish). Chapter 7 of the Spec# tutorial talks about pure methods and alternatives for abstraction, but it seems not to specifically go into
the interaction between pure methods and invariants. Let me try to explain.
The pure method get_a() above will give rise to an axiom of the form:
(forall obj :: Precondition_of_get_a(obj) ==> obj.get_a() == obj._a)
So, in contexts where the precondition of get_a() holds, there is no difference between saying obj.get_a() and saying obj._a (for any object obj). I suspect that this coincides with your expectation. However, let's think about what the precondition
of obj.get_a() is. As explained in section 7.0 of the tutorial, pure methods use
peer validity as their precondition. In other words, the precondition says that the receiver and all its peers must be in the valid state. Remember, being
valid essentially says that the object's invariant has been checked; more precisely, an object becomes valid at the end of constructors and at the end of expose statements, where the invariant is checked.
These details matter whenever you try to establish an invariant. At the end of constructor A() above, _a has been set to 1 and Spec# is about to check the invariant so that it can then mark the object as being valid. It then tries to prove 0
<= get_a(), which means it needs to apply the definition of get_a(), but the definition of get_a() is of no use unless one can discharge the precondition of get_a(), and the precondition is that 'this' is peer valid, but 'this' is currently in the process
of becoming valid and it is not yet valid! So, the antecedent in the axiom about get_a() does not hold, hence the verifier knows nothing about what get_a() returns, and hence you get an error that the object invariant cannot be verified.
In contrast, consider the constructor for B in your example. The B constructor (which in this example is the default constructor provided by the compiler) allocates a new A object and then wants to check the invariant of B. This will work fine,
because at that point, the A object is peer valid (it's even peer consistent), so the antecedent of the axiom for get_a() holds, the verifier gets to know that a.get_a() equals a._a, and the postcondition of the A() constructor says 0 <= a._a, so the verifier
is able to prove B's invariant to hold.
My recommendation would be not to use pure methods in invariants. Instead, refer directly to the _a field there--after all, the invariant speaks about internal things, so there seems to be nothing wrong with talking about _a there.
But in pre- and postconditions of methods, it may be nice to use some abstraction, like get_a(). For example, you may wish to change the postcondition of the A() constructor above to 0 <= get_a(). Section 7 tells you how
to do that (I'm afraid that's not super easy either, but it is doable). For that purpose, you may also consider using model fields instead of pure methods; section 7 explains some differences between the alternatives.
I see. In that case, the problem is easily fixed, but it requires a lot of insight to understand why the code above doesn't work as expected.
However, an invariant is also a postcondition of each method. Thus, it seems that either the syntax for postconditions can be consistent, using no pure methods, or the syntax for pre- and postconditions excluding invariants can be consistent, using only