Lab for Automated Reasoning and Analysis 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.
  
 
sav08/forward_vcg.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice