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:22]
vkuncak
@@ Line 86: / Line 86: @@
-===== Example =====
-Let's take a small example with precondition: $\{x \ge 5 \wedge y \ge 3\}$ and code:
+===== Examples =====
+**Example 1.**
+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}
+\]
+**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
 \]