• English only

# Differences

This shows you the differences between two versions of the page.

sav08:backward_vcg [2009/03/12 12:47]
vkuncak
sav08:backward_vcg [2015/04/21 17:30] (current)
Line 6: Line 6:

We derive the rules below from the definition of weakest precondition on sets and relations 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 \} ​wp(r,​Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \} -$+\end{equation*}

=== Assume Statement === === Assume Statement ===
Line 14: Line 14:
Suppose we have one variable x, and identify state with that variable. Suppose we have one variable x, and identify state with that variable.
By definition By definition
-$+\begin{equation*} \begin{array}{rl} \begin{array}{rl} ​wp(\Delta_F,​Q) & = \{s \mid \forall s'. (s,s') \in \Delta_F \rightarrow s' \in Q \} \\ ​wp(\Delta_F,​Q) & = \{s \mid \forall s'. (s,s') \in \Delta_F \rightarrow s' \in Q \} \\ Line 20: Line 20: & = \{ s \mid s \in F \rightarrow s \in Q \} & = \{ s \mid s \in F \rightarrow s \in Q \} \end{array} \end{array} -$+\end{equation*}
Changing from sets to formulas (and keeping the same name), we obtain the rule for wp on formulas: 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) ​wp(assume(F),​ Q) = (F \rightarrow Q) -$+\end{equation*}

=== Assignment Statement === === Assignment Statement ===

Consider the case of two variables. ​ Recall that the relation associated with the assignment x=e is Consider the case of two variables. ​ Recall that the relation associated with the assignment x=e is
-$+\begin{equation*} ​x'​ = e \land y' = y ​x'​ = e \land y' = y -$+\end{equation*}
Then we have, for formula $Q$ containing $x$ and $y$: Then we have, for formula $Q$ containing $x$ and $y$:
-$+\begin{equation*} \begin{array}{rl} \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'​] \} \\ ​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] \} & = \{(x,y) \mid Q[x:=e] \} \end{array} \end{array} -$ +\end{equation*}
-From here we obtain ​for formulas+From here we obtain:
-$+\begin{equation*} wp(x = e, Q) = Q[x:=e] wp(x = e, Q) = Q[x:=e] -$+\end{equation*}

=== Havoc Statement === === Havoc Statement ===

-$+\begin{equation*} ​wp({\it havoc}(x),​Q) = \forall x.Q ​wp({\it havoc}(x),​Q) = \forall x.Q -$+\end{equation*}

=== Sequential Composition === === Sequential Composition ===

-$+\begin{equation*} ​wp(r_1 \circ r_2, Q) = wp(r_1, wp(r_2, Q)) ​wp(r_1 \circ r_2, Q) = wp(r_1, wp(r_2, Q)) -$+\end{equation*}
Same for formulas: Same for formulas:
-$+\begin{equation*} wp(c_1\ ;\ c_2, Q) = wp(c_1, wp(c_2, Q)) wp(c_1\ ;\ c_2, Q) = wp(c_1, wp(c_2, Q)) -$+\end{equation*}

=== Nondeterministic Choice (Branches) === === Nondeterministic Choice (Branches) ===

In terms of sets and relations In terms of sets and relations
-$+\begin{equation*} wp(r_1 \cup r_2, Q) = wp(r_1,Q) \cap wp(r_2, Q) wp(r_1 \cup r_2, Q) = wp(r_1,Q) \cap wp(r_2, Q) -$+\end{equation*}
In terms of formulas In terms of formulas
-$+\begin{equation*} ​wp(c_1 [] c_2, Q) = wp(c_1,Q) \land wp(c_2,Q) ​wp(c_1 [] c_2, Q) = wp(c_1,Q) \land wp(c_2,Q) -$+\end{equation*}

===== Size of Generated Verification Conditions ===== ===== Size of Generated Verification Conditions =====