# Compositional VCG

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 by formula ## 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.

#### Assignment #### Assume #### Havoc For simplicity of notation, in the sequel we work with state that has only one variable, x.

#### Union

Note Therefore, #### Sequential composition

Note that Therefore, 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.

Resulting formula: 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 #### Example

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