• English only

# Differences

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

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.