# Differences

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

 sav08:backward_vcg [2009/03/12 12:47]vkuncak sav08:backward_vcg [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/03/12 12:48 vkuncak 2009/03/12 12:47 vkuncak 2009/03/12 12:45 vkuncak 2009/03/12 12:43 vkuncak 2009/03/12 12:41 vkuncak 2008/03/04 22:30 vkuncak 2008/03/04 19:20 vkuncak 2008/03/04 19:05 vkuncak 2008/03/04 18:54 vkuncak 2008/03/04 18:54 vkuncak 2008/03/04 18:15 vkuncak 2008/03/03 21:29 maria format2008/03/03 19:33 maria Assume Statement and Assign Statement2008/03/02 22:08 vkuncak created Next revision Previous revision 2009/03/12 12:48 vkuncak 2009/03/12 12:47 vkuncak 2009/03/12 12:45 vkuncak 2009/03/12 12:43 vkuncak 2009/03/12 12:41 vkuncak 2008/03/04 22:30 vkuncak 2008/03/04 19:20 vkuncak 2008/03/04 19:05 vkuncak 2008/03/04 18:54 vkuncak 2008/03/04 18:54 vkuncak 2008/03/04 18:15 vkuncak 2008/03/03 21:29 maria format2008/03/03 19:33 maria Assume Statement and Assign Statement2008/03/02 22:08 vkuncak created 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 =====