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

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.