LARA

Differences

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

Link to this comparison view

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.