Compositional Verification Condition Generator
Rules for Computing Formulas for Commands Compositionally
We compute for each command the formula . We next show how to do it. These rules all follow from the semantics of our language.
For simplicity of notation, in the sequel we work with state that has only one variable, x.
Above, denotes taking formula and replacing in it occurrences of variables by variables .
To avoid re-using variables, introduce always a fresh variable as and denote it .
The semantics for loops is given using transitive closure.
To express this, we would need a logic that supports transitive closure.
If we do this, our formulas will look very much like the programs and there are few good techniques for reasoning about them.
We will therefore deal with loops using alternative techniques (to be discussed later). A simple technique is unrolling loops.
Take the program in the example below:
(if (x < 0) x=x+1 else x=x); (if (y < 0) y=y+x else y=y);
It translates into the following guarded command language:
Computing for basic commands we obtain:
Applying innermost sequential compositions, we obtain
We similarly obtain
Thus, the meaning of the first if statement is:
We can similarly show that the meaning of the second 'if' statement is:
By applying renamings to in first formula and in the second formula, we obtain:
Note that, even if we had left the existential quantifiers over inside, we would be able to lift them to the top level through .
Useful Consequences of Rules
If is a formula containing only unprimed variables, let denote the formula where all program variables become primed ( is replaced by ). More precisely
We then have the following:
Formula Simplification: One-Point Rule
Assignments and assume statements generate equalities, many of which can be eliminated by one-point rule
There are more complex quantifier elimination procedures that can be used in principle as well.
Shape of Generated Formulas
Theorem: Consider a loop-free program . Then each formula generated using the rules above is equivalent to
where are formulas corresponding to havoc,assume (and assignment) statements (with some variables renamed), and denotes a propositional combination that uses only , and where the free variable in the above formula are unprimed and primed program variables. The resulting formula is polynomial in the size of .
Proof: By induction on the structure of . The base cases is trivial, taking to be the formula defining the relation. For the case of non-deterministic choice the property follows easily by lifting existential quantifiers to the top level and taking disjunction of the combinations . Similarly for sequential composition, where we do variable renaming and take conjunction of the combinations .
To see that the 'compositional approach' generates a formula polynomial in the size of the program. Fix the set of variables . Then:
- the size of formula for each basic command is constant
- non-deterministic choice is disjunction
- sequential composition is conjunction (along with renaming that does not affect size)
Moreover, formula generated in such a way looks very much like the program itself, converted to static single assignment form, see
Using Computed Formulas to Obtain Verification Conditions
Suppose we wish to prove
The resulting formula has the form:
which is equivalent to
If we generate fresh variables for intermediate points, it suffices to prove the validity of the quantifier free formula:
Equivalently, we need to prove unsatisfiability of the formula