8. Verification code must be erasable
To support goal 7, for verification code not to affect the outcome of executing the program, Laurel has rules for code that exists only for verification purposes.
Rules for contracts:
-
Contract code may not modify variables defined outside the contract scope.
-
Contract code has an empty modifies clause. Contract code operates on a copy of the heap.
-
Contract code must terminate, so removing it does not affect whether execution code is reachable or not.
For example, the body of the procedure below changes p, and that effect is declared with
modifies p; old(p#x) in the ensures clause refers to the pre-state:
procedure shift(p: Point, dx: int)
opaque
ensures p#x == old(p#x) + dx
modifies p
{
p#x := p#x + dx
};
The ensures expression may read the heap and build temporary values while it is evaluated, but it
cannot assign to p, to dx, or to any variable declared outside it, and it contributes no
modifies effect of its own. Even if the postcondition called a helper that allocated and mutated a
scratch object, that would run against a copy of the heap and remain invisible to callers, which
still see every pre-existing object unchanged across the evaluation of the contract. As a result,
adding, strengthening, or removing the ensures clause never changes how the program executes.