Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:forward_vcg [2009/03/10 20:35] vkuncak |
sav08:forward_vcg [2009/03/10 20:50] vkuncak |
||
---|---|---|---|
Line 35: | Line 35: | ||
= \{s' | s' \in P_s, s' \in F_s\} = P_s \cap F_s. | = \{s' | s' \in P_s, s' \in F_s\} = P_s \cap F_s. | ||
\end{array} | \end{array} | ||
+ | \] | ||
+ | |||
+ | === Havoc Statement === | ||
+ | |||
+ | Define: | ||
+ | \[ | ||
+ | sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0] | ||
\] | \] | ||
Line 41: | Line 48: | ||
Define: | 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)]) \} | = \{s'| \exists s.(s \in P_s \wedge s' = s[x \rightarrow f_T(e)(s)]) \} | ||
\end{array} | \end{array} | ||
- | \] | ||
- | |||
- | === Havoc Statement === | ||
- | |||
- | Define: | ||
- | \[ | ||
- | sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0] | ||
\] | \] | ||
Line 78: | Line 78: | ||
\] | \] | ||
- | ==== Correctness ==== | + | ===== Correctness ===== |
We show by induction on $c_1$ that for all $P$: | We show by induction on $c_1$ that for all $P$: | ||
Line 86: | Line 86: | ||
- | ==== Example ==== | ||
- | Let's take a small example with precondition: $\{x=0 \wedge y=0\}$ and code: | + | |
+ | ===== Example ===== | ||
+ | |||
+ | Let's take a small example with precondition: $\{x \ge 5 \wedge y \ge 3\}$ and code: | ||
<code> | <code> | ||
- | x = x+1; | + | x = x + y + 10 |
</code> | </code> | ||
\[ | \[ | ||
- | sp(x=0 \wedge y=0, x=x+1) = \exists x_0.(x = x_0+1 \wedge y=0 \wedge x_0 = 0). | + | \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} | ||
\] | \] | ||