Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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