This is an old revision of the document!
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 \[
sp(\{s.\ f_T(P)(s)\}, r_c(c_1)) = \{ s.\ f_T(sp_F(P,c_1))(s) \}
\] or, less formally, \[
sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \}
\]
For a predicate , let be the set of states that satisfies it, \[ P_s = \{s.\ f_T(P)(s) \} \]
Rules for Computing Strongest Postcondition
Assume Statement
Define: \[
sp_F(P, assume(F)) = P \wedge F
\]
Then \[ \begin{array}{l}
sp(P_s, assume(F)) \\ = sp(P_s, \Delta_{F_s}) \\ = \{s' | \exists s \in P_s.((s,s') \in \Delta_{F_s})\} \\ = \{s' | \exists s \in P_s.(s=s' \wedge s \in F_s)\} \\ = \{s' | s' \in P_s, s' \in F_s\} = P_s \cap F_s.
\end{array} \]
Assignment Statement
Define: \[
sp_F(P, x = e) = \exists x_0.(x=e[x:=x_0] \wedge P[x:=x_0])
\]
Indeed: \[ \begin{array}{l}
sp(P_s, r_c(x = e)) \\ = \{s'| \exists s.(s \in P_s \wedge (s, s') \in r_c(x=e))\} \\ = \{s'| \exists s.(s \in P_s \wedge s' = s[x \rightarrow f_T(e)(s)]) \}
\end{array} \]
Havoc Statement
Define: \[
sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0]
\]
Sequential Composition
For relations we proved \[
sp(P_s,r_1 \circ r_2) = sp(sp(P_s,r_1),r_2)
\] Therefore, define \[
sp_F(P,c_1;c_2) = sp_F(sp_F(P,c_1),c_2)
\]
Nondeterministic Choice (Branches)
We had . Therefore define: \[
sp_F(P,c_1 [] c_2) = sp_F(P,c_1) \lor sp_F(P,c_2)
\]
Correctness
We show by induction on that for all : \[
sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \}
\]
Example
Let's take a small example with precondition: and code:
x = x + y+10;
\[ sp(x \ge 5 \land y \ge 3, x=x+1) = \exists x_0.\ x_0 \ge 5 \wedge y \ge 3\ \land\ x = x_0 + y \]
Size of Generated Formulas
The size of the formula can be exponential because each time we have a nondeterministic choice, we double formula size:
\[
\begin{array}{l}
sp_F(P, (c_1 [] c_2);(c_3 [] c_4)) =
sp_F(sp_F(P,c_1 [] c_2), c_3 [] c_4) =
sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_3 [] c_4) =
sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_3) \vee
sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_4)
\end{array}
\]
Reducing sp to Relation Composition
The following identity holds for relations (see Sets and Relations): \[
sp(P,r) = ran(\Delta_P \circ r)
\]
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, \[
r_1 = \{(\vec x, \vec x\,').\ F_1(\vec x,\vec x\,')
\] then is formula denoting the range of : \[
ran(r_1) = \{ \vec x\,'.\ \exists \vec x. F_1(\vec x, \vec x\,') \}
\] Moreover, the resulting approach does not have exponentially large formulas.