An invariant of an object is admissible
if it cannot be broken by changes to other objects, provided those changes preserve invariants of those objects.
VCC enforces admissibility of invariants by means of extra proof obligations. For each type
with invariants we generate a special function named
. The function gets an
pointer to type T
as parameter, and then calls a special procedure
. This procedure simulates changes to other objects.
Let S0 be the pre-state of the function and S1 be the state after
. The contract of havoc_others(...)
specifies that for all objects, spans of which did change between S0 and S1, if they are closed in either S0 or S1 then their two state invariant holds across S0->S1
Additionally it specifies that p
was closed in both S0 and S1, and that the two state invariant of
holds in S0 repeated.
There are two proof obligations there:
1. the two state invariant of p
holds across S0->S1 (stability)
2. the two state invariant of p
holds in S1 repeated (stuttering)
This is enforced by means of postconditions on the admissibility check function.
It is also possible to specify custom admissibility checks, see
Invariants of objects usually talk about states when the object is closed in the post state. Such invariants are checked when wrapping objects (i.e. the transition from open to closed state) and then are preserved by admissibility.
It is however also possible to specify invariant that need to hold when opening the object. The typical use of that is to restrict opening of objects. However unrestricted use of this feature forces us to check all the invariant when unwrapping the object (while
at the meta level we know that most of them will hold, because they did hold in pre-state of unwrap). Because this places additional burden on the prover, invariants that restrict opening of the object need to be specifically marked, instead of saying:
invariant(old(closed(this)) && !closed(this) ==> ...)
you need to say:
(leaving out invariant(...)
Only such conditions are checked when unwrapping objects, however for soundness we need to guarantee that no other invariants can be broken when unwrapping objects. This proof obligation is present in the code in form of the
function, which is syntactically much like the admissibility check: it is a function taking a closed object
of type T
, which calls (something reassembling)
, and then checks two states invariants of
across that transition.
Admissibility of claims
implies one-state invariants of all closed objects including claims.
implies that everything a closed object owns is closed and everything protected by a closed claim is closed.
When proving admissibility of an ordinary type you get to assume:
- full_stop of the pre-state
- two-state invariants of changed, closed objects between pre- and post-state
- good_state for both pre- and post-state
- the object in question is closed in both pre- and post-state and its span didn't change
When proving admissibility of a claim you get to assume:
- everything as in the standard admissibility check
- invariants of all closed ordinary types in the post-state
- invariants of claims that are closed now and were closed before the current claim was created in the post-state
The statement claims(c, prop)
is translated as
forall(state S; valid_claim(S, c) ==> prop(S))
is usually proven from:
forall(S,c; full_stop(S) && closed(S, c) ==> valid_claim(S, c))
If claims(c, prop)
occurs in an invariant, it's subject to standard admissibility check, but this is usually easy, as it does not refer to the current state, and thus is exactly the same in the pre- and post-state. On the
other hand, as the post-state in admissibility check is not a full_stop state, this statement cannot be used to help prove admissibility of the rest of the invariant.
When proving admissibility of a claim taken in state s0, between states s1 and s2, we include the following assumption:
forall(claim_t c; closed(s0, c) && closed(s2, c) ==> valid_claim(s2, c))
This allows for using properties of earlier claims when proving admissibility of a later claim.
If the claim is taken inside of an atomic action (alter block), then the initial check of a claim condition is performed just before checking invariants of all modified objects. After this check is done, the claims(c, prop) is assumed (and thus when checking
invariants of modified objects, it can be used, in the sense of satisfying claims(c, prop) in an invariant, but not in the sense of prop).