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
For relations we proved
Nondeterministic Choice (Branches)
We had . Therefore define:
We show by induction on that for all :
Example 1. Precondition: . Code:
x = x + y + 10
Example 2. Precondition: . Code:
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.