Let be formulas and a command of our language using variables . To check we compute formula containing specifying the semantics of c_1, that is, formula such that
Denote the truth value of formula in two states by (predicate for the formula) using an auxiliary definition of (function for the term):
Then we can construct formula such that . Denote such formula by . To can then represent the validity of a Hoare triple
Rules for Computing Formulas for Commands
Therefore, to prove Hoare triples, we just need to 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 .
Using Computed Formulas
Note: the result will be disjunctions of such existential quantifications. We can always move them to top level.
which is equivalent to
Conclusions: we can just generate fresh variables for intermediate points and prove the validity of the resulting quantifier free formula .
Optimizations: assignments and assume statements generate equalities, many of which can be eliminated by one-point rule
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 translate into the following relation:
By distribution of composition over union the relation above becomes:
It can be easily proven that :
We can take all the terms of the union one by one as in the following small example:
Using valid formulas we can move the existential quantifiers outside the formula.
However, we can avoid expanding all paths and instead compute relations by following program structure.
Size of Generated Formulas
The compositional approach generates a formula polynomial in the size of the program. Indeed, 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–or affects at most )
Moreover, formula generated in such a way looks very much like the program itself, converted to static single assignment form, see