Differences

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

--- sav08:forward_vcg [2009/03/10 20:46]
vkuncak
+++ sav08:forward_vcg [2010/03/09 17:18]
vkuncak
@@ Line 35: / Line 35: @@
    = \{s' | s' \in P_s, s' \in F_s\} = P_s \cap F_s.
 \end{array}
+\]
+=== Havoc Statement ===
+Define:
+\[
+   sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0]
 \]
@@ Line 41: / Line 48: @@
 Define:
 \[
-   sp_F(P, x = e) = \exists x_0.(x=e[x:=x_0] \wedge P[x:=x_0])
+   sp_F(P, x = e) = \exists x_0.(P[x:=x_0] \land x=e[x:=x_0])
 \]
@@ Line 51: / Line 58: @@
    = \{s'| \exists s.(s \in P_s \wedge s' = s[x \rightarrow f_T(e)(s)]) \}
 \end{array}
-\]
-=== Havoc Statement ===
-Define:
-\[
-   sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0]
 \]
@@ Line 84: / Line 84: @@
    sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \}
 \]
 ===== Example =====
-Let's take a small example with precondition: $\{x \ge 5 \wedge y \ge 3\}$ and code:
+Precondition: $\{x \ge 5 \wedge y \ge 3\}$. Code:
 <code>
-x = x + y+10;
+x = x + y + 10
 </code>
 \[
-sp(x \ge 5 \land y \ge 3, x=x+1) = \exists x_0.\ x_0 \ge 5 \wedge y \ge 3\ \land\ x = x_0 + y
+\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}
 \]