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.

Admissibility check

VCC enforces admissibility of invariants by means of extra proof obligations. For each type T with invariants we generate a special function named $admissibility_T. The function gets an p pointer to type T as parameter, and then calls a special procedure havoc_others(p). This procedure simulates changes to other objects.

Let S0 be the pre-state of the function and S1 be the state after havoc_others(p). 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 transition.

Additionally it specifies that p was closed in both S0 and S1, and that the two state invariant of p 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 Admissibility annotations.

Unwrap check

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:

on_unwrap(...)

(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 $unwrap_T function, which is syntactically much like the admissibility check: it is a function taking a closed object p of type T, which calls (something reassembling) unwrap(p), and then checks two states invariants of p across that transition.

Admissibility of claims

full_stop(S) implies one-state invariants of all closed objects including claims.

good_state(S) 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)).

valid_claim 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).

Last edited Nov 13, 2009 at 1:05 PM by stobies, version 4

Comments

No comments yet.