# 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

#### Assume Statement

Define:

Then

#### Havoc Statement

Define:

#### Assignment Statement

Define:

Indeed:

#### Sequential Composition

For relations we proved

Therefore, define

#### Nondeterministic Choice (Branches)

We had . 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:

- compute formula , using Compositional VCG
- 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.