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

#### Havoc

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

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