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]
Line 1: Line 1:
-====== Backward VCG: Symbolic Execution using Weakest Preconditions ====== 
- 
-We again assume for simplicity to have two variables, $V = \{ x,y \}$. 
- 
-===== Rules for Computing Weakest Preconditions ===== 
- 
-We derive the rules below from the definition of weakest precondition on sets and relations 
-\[ 
-   ​wp(r,​Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \} 
-\] 
- 
-=== Assume Statement === 
- 
-Suppose we have one variable x, and identify state with that variable. 
-By definition 
-\[ 
-\begin{array}{rl} 
-   ​wp(\Delta_F,​Q) & = \{s \mid \forall s'. (s,s') \in \Delta_F \rightarrow s' \in Q \} \\ 
-                  & = \{ s \mid \forall s'. (s \in F \land s=s') \rightarrow s' \in Q \} \\ 
-                  & = \{ s \mid s \in F \rightarrow s \in Q \} 
-\end{array} 
-\] 
-Changing from sets to formulas (and keeping the same name), we obtain the rule for wp on formulas: 
-\[ 
-   ​wp(assume(F),​ Q) = (F \rightarrow Q) 
-\] 
- 
-=== Assignment Statement === 
- 
-Consider the case of two variables. ​ Recall that the relation associated with the assignment x=e is 
-\[ 
-   ​x'​ = e \land y' = y 
-\] 
-Then we have, for formula $Q$ containing $x$ and $y$: 
-\[ 
-\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'​] \} \\ 
-                                 & = \{(x,y) \mid Q[x:=e] \} 
-\end{array} 
-\] 
-From here we obtain for formulas: 
-\[ 
-   wp(x = e, Q) = Q[x:=e] 
-\] 
- 
-=== Havoc Statement === 
- 
-\[ 
-   ​wp({\it havoc}(x),​Q) = \forall x.Q 
-\] 
- 
-=== Sequential Composition === 
- 
-\[ 
-     ​wp(r_1 \circ r_2, Q) = wp(r_1, wp(r_2, Q)) 
-\] 
-Same for formulas: 
-\[ 
-    wp(c_1\ ;\ c_2, Q) = wp(c_1, wp(c_2, Q)) 
-\] 
- 
-=== Nondeterministic Choice (Branches) === 
- 
-In terms of sets and relations 
-\[ 
-    wp(r_1 \cup r_2, Q) = wp(r_1,Q) \cap wp(r_2, Q) 
-\] 
-In terms of formulas 
-\[ 
-   ​wp(c_1 [] c_2, Q) = wp(c_1,Q) \land wp(c_2,Q) 
-\] 
- 
-===== Size of Generated Verification Conditions ===== 
- 
-Because of the rule $wp(c_1 [] c_2, Q) = wp(c_1,Q) \land wp(c_2,Q)$ which duplicates $Q$, the size can be exponential. 
- 
-=== More information === 
- 
-  * [[Calculus of Computation Textbook]], Chapter 5 (Program Correctness:​ Mechanics)