Backward VCG: Symbolic Execution using Weakest Preconditions

We again assume for simplicity to have two variables, $V = \{ x,y \}$ .

Rules for Computing Weakest Preconditions

We derive the rules below from the definition of weakest precondition on sets and relations

$\begin{equation*} wp(r,Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \} \end{equation*}$

Assume Statement

Suppose we have one variable x, and identify state with that variable. By definition

$\begin{equation*} \begin{array}{rl} wp(\Delta_F,Q) & = \{s \mid \forall s'. (s,s') \in \Delta_F \rightarrow s' \in Q \} \\ & = \{ s \mid \forall s'. (s \in F \land s=s') \rightarrow s' \in Q \} \\ & = \{ s \mid s \in F \rightarrow s \in Q \} \end{array} \end{equation*}$

Changing from sets to formulas (and keeping the same name), we obtain the rule for wp on formulas:

$\begin{equation*} wp(assume(F), Q) = (F \rightarrow Q) \end{equation*}$

Assignment Statement

Consider the case of two variables. Recall that the relation associated with the assignment x=e is

$\begin{equation*} x' = e \land y' = y \end{equation*}$

Then we have, for formula $Q$ containing $x$ and $y$ :

$\begin{equation*} \begin{array}{rl} wp(r_c(x=e),\{(x,y) \mid Q\}) & = \{(x,y) \mid \forall x'.\forall y'.\ x'=e \land y'=y \rightarrow Q[x:=x',y:=y'] \} \\ & = \{(x,y) \mid Q[x:=e] \} \end{array} \end{equation*}$