Differences

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

--- sav08:forward_vcg [2010/03/09 17:18]
vkuncak
+++ sav08:forward_vcg [2010/03/09 17:24]
vkuncak
@@ Line 89: / Line 89: @@
-===== Example =====
+===== Examples =====
+**Example 1.**
 Precondition: $\{x \ge 5 \wedge y \ge 3\}$. Code:
 <code>
@@ Line 103: / Line 108: @@
 \end{array}
 \]
+**Example 2.** Precondition: $\{x \ge 2 \land y \le 5 \land x \le y \}$. Code:
+<code>
+havoc(x)
+</code>
+\[
+  \exists x_0.\ x_0 \ge 2 \land y \le 5 \land x_0 \le y
+\]
+i.e.
+\[
+   \exists x_0.\ 2 \le x_0 \le y \land y \le 5
+\]
+i.e.
+\[
+\le y \land y \le 5
+\]
+If we simply removed conjuncts containing $x$, we would get just $y \le 5$.
 ===== Size of Generated Formulas =====