LARA

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*}

Reducing sp to Relation Composition

The following identity holds for relations (see Sets and Relations):

\begin{equation*}
   sp(P,r) = ran(\Delta_P \circ r)
\end{equation*}

Based on this, we can compute $sp(P,c_1)$ in two steps:

  1. compute formula $F_c(assume(P);c_1)$, using Compositional VCG
  2. existentially quantify over initial (non-primed) variables

Indeed, if $F_1$ is a formula denoting relation $r_1$, that is,

\begin{equation*}
    r_1 = \{(\vec x, \vec x\,').\ F_1(\vec x,\vec x\,')
\end{equation*}

then $\ \exists \vec x. F_1(\vec x, \vec x\,')$ is formula denoting the range of $r_1$:

\begin{equation*}
   ran(r_1) = \{ \vec x\,'.\ \exists \vec x. F_1(\vec x, \vec x\,') \}
\end{equation*}

Moreover, the resulting approach does not have exponentially large formulas.