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:backward_vcg [2009/03/12 12:47]
vkuncak
sav08:backward_vcg [2015/04/21 17:30] (current)
Line 6: Line 6:
  
 We derive the rules below from the definition of weakest precondition on sets and relations We derive the rules below from the definition of weakest precondition on sets and relations
-\[+\begin{equation*}
    ​wp(r,​Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \}    ​wp(r,​Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \}
-\]+\end{equation*}
  
 === Assume Statement === === Assume Statement ===
Line 14: Line 14:
 Suppose we have one variable x, and identify state with that variable. Suppose we have one variable x, and identify state with that variable.
 By definition By definition
-\[+\begin{equation*}
 \begin{array}{rl} \begin{array}{rl}
    ​wp(\Delta_F,​Q) & = \{s \mid \forall s'. (s,s') \in \Delta_F \rightarrow s' \in Q \} \\    ​wp(\Delta_F,​Q) & = \{s \mid \forall s'. (s,s') \in \Delta_F \rightarrow s' \in Q \} \\
Line 20: Line 20:
                   & = \{ s \mid s \in F \rightarrow s \in Q \}                   & = \{ s \mid s \in F \rightarrow s \in Q \}
 \end{array} \end{array}
-\]+\end{equation*}
 Changing from sets to formulas (and keeping the same name), we obtain the rule for wp on formulas: Changing from sets to formulas (and keeping the same name), we obtain the rule for wp on formulas:
-\[+\begin{equation*}
    ​wp(assume(F),​ Q) = (F \rightarrow Q)    ​wp(assume(F),​ Q) = (F \rightarrow Q)
-\]+\end{equation*}
  
 === Assignment Statement === === Assignment Statement ===
  
 Consider the case of two variables. ​ Recall that the relation associated with the assignment x=e is Consider the case of two variables. ​ Recall that the relation associated with the assignment x=e is
-\[+\begin{equation*}
    ​x'​ = e \land y' = y    ​x'​ = e \land y' = y
-\]+\end{equation*}
 Then we have, for formula $Q$ containing $x$ and $y$: Then we have, for formula $Q$ containing $x$ and $y$:
-\[+\begin{equation*}
 \begin{array}{rl} \begin{array}{rl}
    ​wp(r_c(x=e),​\{(x,​y) \mid Q\}) & = \{(x,y) \mid \forall x'​.\forall y'.\ x'=e \land y'=y \rightarrow Q[x:​=x',​y:​=y'​] \} \\    ​wp(r_c(x=e),​\{(x,​y) \mid Q\}) & = \{(x,y) \mid \forall x'​.\forall y'.\ x'=e \land y'=y \rightarrow Q[x:​=x',​y:​=y'​] \} \\
                                  & = \{(x,y) \mid Q[x:=e] \}                                  & = \{(x,y) \mid Q[x:=e] \}
 \end{array} \end{array}
-\] +\end{equation*} 
-From here we obtain ​for formulas+From here we obtain: 
-\[+\begin{equation*}
    wp(x = e, Q) = Q[x:=e]    wp(x = e, Q) = Q[x:=e]
-\]+\end{equation*}
  
 === Havoc Statement === === Havoc Statement ===
  
-\[+\begin{equation*}
    ​wp({\it havoc}(x),​Q) = \forall x.Q    ​wp({\it havoc}(x),​Q) = \forall x.Q
-\]+\end{equation*}
  
 === Sequential Composition === === Sequential Composition ===
  
-\[+\begin{equation*}
      ​wp(r_1 \circ r_2, Q) = wp(r_1, wp(r_2, Q))      ​wp(r_1 \circ r_2, Q) = wp(r_1, wp(r_2, Q))
-\]+\end{equation*}
 Same for formulas: Same for formulas:
-\[+\begin{equation*}
     wp(c_1\ ;\ c_2, Q) = wp(c_1, wp(c_2, Q))     wp(c_1\ ;\ c_2, Q) = wp(c_1, wp(c_2, Q))
-\]+\end{equation*}
  
 === Nondeterministic Choice (Branches) === === Nondeterministic Choice (Branches) ===
  
 In terms of sets and relations In terms of sets and relations
-\[+\begin{equation*}
     wp(r_1 \cup r_2, Q) = wp(r_1,Q) \cap wp(r_2, Q)     wp(r_1 \cup r_2, Q) = wp(r_1,Q) \cap wp(r_2, Q)
-\]+\end{equation*}
 In terms of formulas In terms of formulas
-\[+\begin{equation*}
    ​wp(c_1 [] c_2, Q) = wp(c_1,Q) \land wp(c_2,Q)    ​wp(c_1 [] c_2, Q) = wp(c_1,Q) \land wp(c_2,Q)
-\]+\end{equation*}
  
 ===== Size of Generated Verification Conditions ===== ===== Size of Generated Verification Conditions =====
 
sav08/backward_vcg.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice