Forward VCG: Using Strongest Postcondition

If is a formula on state and a command, let the formula version of strongest postcondition operator. is therefore formula that describes the set of states that can result from executing in a state satisfying .

Thus, we have

or, less formally,

For a predicate , let be the set of states that satisfies it,

Rules for Computing Strongest Postcondition

Define:

Then

Define:

Define:

Indeed:

Sequential Composition

For relations we proved

Therefore, define

Correctness

We show by induction on that for all :

Examples

Example 1. Precondition: . Code:

x = x + y + 10

Example 2. Precondition: . Code:

havoc(x)

i.e.

i.e.

If we simply removed conjuncts containing , we would get just .

Size of Generated Formulas

The size of the formula can be exponential because each time we have a nondeterministic choice, we double formula size:

Reducing sp to Relation Composition

The following identity holds for relations (see Sets and Relations):

Based on this, we can compute in two steps:

1. compute formula , using Compositional VCG
2. existentially quantify over initial (non-primed) variables

Indeed, if is a formula denoting relation , that is,

then is formula denoting the range of :

Moreover, the resulting approach does not have exponentially large formulas.