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
-\[
+\begin{equation*}
    wp(r,Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \}
-\]
+\end{equation*}
 === Assume Statement ===
@@ Line 14: / Line 14: @@
 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 \} \\
@@ Line 20: / Line 20: @@
                   & = \{ 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*}
-From here we obtain for formulas:
+From here we obtain:
-\[
+\begin{equation*}
    wp(x = e, Q) = Q[x:=e]
-\]
+\end{equation*}
 === Havoc Statement ===
-\[
+\begin{equation*}
    wp({\it havoc}(x),Q) = \forall x.Q
-\]
+\end{equation*}
 === Sequential Composition ===
-\[
+\begin{equation*}
      wp(r_1 \circ r_2, Q) = wp(r_1, wp(r_2, Q))
-\]
+\end{equation*}
 Same for formulas:
-\[
+\begin{equation*}
     wp(c_1\ ;\ c_2, Q) = wp(c_1, wp(c_2, Q))
-\]
+\end{equation*}
 === Nondeterministic Choice (Branches) ===
 In terms of sets and relations
-\[
+\begin{equation*}
     wp(r_1 \cup r_2, Q) = wp(r_1,Q) \cap wp(r_2, Q)
-\]
+\end{equation*}
 In terms of formulas
-\[
+\begin{equation*}
    wp(c_1 [] c_2, Q) = wp(c_1,Q) \land wp(c_2,Q)
-\]
+\end{equation*}
 ===== Size of Generated Verification Conditions =====