Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:forward_vcg [2010/03/09 17:23] vkuncak |
sav08:forward_vcg [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 4: | Line 4: | ||
Thus, we have | Thus, we have | ||
- | \[ | + | \begin{equation*} |
sp(\{s.\ f_T(P)(s)\}, r_c(c_1)) = \{ s.\ f_T(sp_F(P,c_1))(s) \} | sp(\{s.\ f_T(P)(s)\}, r_c(c_1)) = \{ s.\ f_T(sp_F(P,c_1))(s) \} | ||
- | \] | + | \end{equation*} |
or, less formally, | or, less formally, | ||
- | \[ | + | \begin{equation*} |
sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \} | sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \} | ||
- | \] | + | \end{equation*} |
For a predicate $P$, let $P_s$ be the set of states that satisfies it, | For a predicate $P$, let $P_s$ be the set of states that satisfies it, | ||
- | \[ | + | \begin{equation*} |
P_s = \{s.\ f_T(P)(s) \} | P_s = \{s.\ f_T(P)(s) \} | ||
- | \] | + | \end{equation*} |
===== Rules for Computing Strongest Postcondition ===== | ===== Rules for Computing Strongest Postcondition ===== | ||
Line 22: | Line 22: | ||
Define: | Define: | ||
- | \[ | + | \begin{equation*} |
sp_F(P, assume(F)) = P \wedge F | sp_F(P, assume(F)) = P \wedge F | ||
- | \] | + | \end{equation*} |
Then | Then | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
sp(P_s, assume(F)) \\ | sp(P_s, assume(F)) \\ | ||
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} | ||
- | \] | + | \end{equation*} |
=== Havoc Statement === | === Havoc Statement === | ||
Define: | Define: | ||
- | \[ | + | \begin{equation*} |
sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0] | sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0] | ||
- | \] | + | \end{equation*} |
=== Assignment Statement === | === Assignment Statement === | ||
Define: | Define: | ||
- | \[ | + | \begin{equation*} |
sp_F(P, x = e) = \exists x_0.(P[x:=x_0] \land x=e[x:=x_0]) | sp_F(P, x = e) = \exists x_0.(P[x:=x_0] \land x=e[x:=x_0]) | ||
- | \] | + | \end{equation*} |
Indeed: | Indeed: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
sp(P_s, r_c(x = e)) \\ | sp(P_s, r_c(x = e)) \\ | ||
Line 58: | 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} | ||
- | \] | + | \end{equation*} |
=== Sequential Composition === | === Sequential Composition === | ||
For relations we proved | For relations we proved | ||
- | \[ | + | \begin{equation*} |
sp(P_s,r_1 \circ r_2) = sp(sp(P_s,r_1),r_2) | sp(P_s,r_1 \circ r_2) = sp(sp(P_s,r_1),r_2) | ||
- | \] | + | \end{equation*} |
Therefore, define | Therefore, define | ||
- | \[ | + | \begin{equation*} |
sp_F(P,c_1;c_2) = sp_F(sp_F(P,c_1),c_2) | sp_F(P,c_1;c_2) = sp_F(sp_F(P,c_1),c_2) | ||
- | \] | + | \end{equation*} |
=== Nondeterministic Choice (Branches) === | === Nondeterministic Choice (Branches) === | ||
We had $sp(P, r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2)$. Therefore define: | We had $sp(P, r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2)$. Therefore define: | ||
- | \[ | + | \begin{equation*} |
sp_F(P,c_1 [] c_2) = sp_F(P,c_1) \lor sp_F(P,c_2) | sp_F(P,c_1 [] c_2) = sp_F(P,c_1) \lor sp_F(P,c_2) | ||
- | \] | + | \end{equation*} |
===== Correctness ===== | ===== Correctness ===== | ||
We show by induction on $c_1$ that for all $P$: | We show by induction on $c_1$ that for all $P$: | ||
- | \[ | + | \begin{equation*} |
sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \} | sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \} | ||
- | \] | + | \end{equation*} |
Line 100: | Line 101: | ||
</code> | </code> | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
sp(x \ge 5 \land y \ge 3, x=x+y+10) = \\ | sp(x \ge 5 \land y \ge 3, x=x+y+10) = \\ | ||
Line 106: | Line 107: | ||
\leftrightarrow \ y \ge 3 \land x \ge y + 15 | \leftrightarrow \ y \ge 3 \land x \ge y + 15 | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
- | **Example 2** Precondition: $\{x \ge 2 \land y \le 5 \land x \le y \}$. Code: | + | **Example 2.** Precondition: $\{x \ge 2 \land y \le 5 \land x \le y \}$. Code: |
<code> | <code> | ||
havoc(x) | havoc(x) | ||
</code> | </code> | ||
- | \[ | + | \begin{equation*} |
\exists x_0.\ x_0 \ge 2 \land y \le 5 \land x_0 \le y | \exists x_0.\ x_0 \ge 2 \land y \le 5 \land x_0 \le y | ||
- | \] | + | \end{equation*} |
i.e. | i.e. | ||
- | \[ | + | \begin{equation*} |
\exists x_0.\ 2 \le x_0 \le y \land y \le 5 | \exists x_0.\ 2 \le x_0 \le y \land y \le 5 | ||
- | \] | + | \end{equation*} |
i.e. | i.e. | ||
- | \[ | + | \begin{equation*} |
2 \le y \land y \le 5 | 2 \le y \land y \le 5 | ||
- | \] | + | \end{equation*} |
If we simply removed conjuncts containing $x$, we would get just $y \le 5$. | If we simply removed conjuncts containing $x$, we would get just $y \le 5$. | ||
Line 129: | Line 130: | ||
The size of the formula can be exponential because each time we have a nondeterministic choice, we double formula size: | The size of the formula can be exponential because each time we have a nondeterministic choice, we double formula size: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
sp_F(P, (c_1 [] c_2);(c_3 [] c_4)) = \\ | sp_F(P, (c_1 [] c_2);(c_3 [] c_4)) = \\ | ||
Line 137: | Line 138: | ||
sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_4) | sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_4) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
===== Reducing sp to Relation Composition ===== | ===== Reducing sp to Relation Composition ===== | ||
The following identity holds for relations (see [[:sav08:Sets and Relations]]): | The following identity holds for relations (see [[:sav08:Sets and Relations]]): | ||
- | \[ | + | \begin{equation*} |
sp(P,r) = ran(\Delta_P \circ r) | sp(P,r) = ran(\Delta_P \circ r) | ||
- | \] | + | \end{equation*} |
Line 153: | Line 154: | ||
Indeed, if $F_1$ is a formula denoting relation $r_1$, that is, | Indeed, if $F_1$ is a formula denoting relation $r_1$, that is, | ||
- | \[ | + | \begin{equation*} |
r_1 = \{(\vec x, \vec x\,').\ F_1(\vec x,\vec x\,') | r_1 = \{(\vec x, \vec x\,').\ F_1(\vec x,\vec x\,') | ||
- | \] | + | \end{equation*} |
then $\ \exists \vec x. F_1(\vec x, \vec x\,')$ is formula denoting the range of $r_1$: | then $\ \exists \vec x. F_1(\vec x, \vec x\,')$ is formula denoting the range of $r_1$: | ||
- | \[ | + | \begin{equation*} |
ran(r_1) = \{ \vec x\,'.\ \exists \vec x. F_1(\vec x, \vec x\,') \} | ran(r_1) = \{ \vec x\,'.\ \exists \vec x. F_1(\vec x, \vec x\,') \} | ||
- | \] | + | \end{equation*} |
Moreover, the resulting approach does not have exponentially large formulas. | Moreover, the resulting approach does not have exponentially large formulas. | ||