Forward VCG: Using Strongest Postcondition

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

Thus, we have

$\begin{equation*} sp(\{s.\ f_T(P)(s)\}, r_c(c_1)) = \{ s.\ f_T(sp_F(P,c_1))(s) \} \end{equation*}$

or, less formally,

$\begin{equation*} sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \} \end{equation*}$

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

$\begin{equation*} P_s = \{s.\ f_T(P)(s) \} \end{equation*}$

Rules for Computing Strongest Postcondition

Assume Statement

Define:

$\begin{equation*} sp_F(P, assume(F)) = P \wedge F \end{equation*}$

Then

$\begin{equation*} \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} \end{equation*}$

Havoc Statement

Define:

$\begin{equation*} sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0] \end{equation*}$

Assignment Statement

Define:

$\begin{equation*} sp_F(P, x = e) = \exists x_0.(P[x:=x_0] \land x=e[x:=x_0]) \end{equation*}$

Indeed:

$\begin{equation*} \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} \end{equation*}$

Sequential Composition

For relations we proved

$\begin{equation*} sp(P_s,r_1 \circ r_2) = sp(sp(P_s,r_1),r_2) \end{equation*}$

Therefore, define

$\begin{equation*} sp_F(P,c_1;c_2) = sp_F(sp_F(P,c_1),c_2) \end{equation*}$

Nondeterministic Choice (Branches)

We had $sp(P, r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2)$ . Therefore define:

$\begin{equation*} sp_F(P,c_1 [] c_2) = sp_F(P,c_1) \lor sp_F(P,c_2) \end{equation*}$

Correctness

We show by induction on $c_1$ that for all $P$ :

$\begin{equation*} sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \} \end{equation*}$

Examples

Example 1. Precondition: $\{x \ge 5 \wedge y \ge 3\}$ . Code:

x = x + y + 10

$\begin{equation*} \begin{array}{l} sp(x \ge 5 \land y \ge 3, x=x+y+10) = \\ \exists x_0.\ x_0 \ge 5 \wedge y \ge 3\ \land\ x = x_0 + y + 10 \\ \leftrightarrow \ y \ge 3 \land x \ge y + 15 \end{array} \end{equation*}$

Example 2. Precondition: $\{x \ge 2 \land y \le 5 \land x \le y \}$ . Code:

havoc(x)

$\begin{equation*} \exists x_0.\ x_0 \ge 2 \land y \le 5 \land x_0 \le y \end{equation*}$

i.e.

$\begin{equation*} \exists x_0.\ 2 \le x_0 \le y \land y \le 5 \end{equation*}$

i.e.

$\begin{equation*} 2 \le y \land y \le 5 \end{equation*}$

If we simply removed conjuncts containing $x$ , we would get just $y \le 5$ .

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{equation*} \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} \end{equation*}$