Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:backward_vcg [2009/03/12 12:45] vkuncak |
sav08:backward_vcg [2009/03/12 12:48] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Backward VCG: Symbolic Execution using Weakest Preconditions ====== | ====== Backward VCG: Symbolic Execution using Weakest Preconditions ====== | ||
| + | |||
| + | We again assume for simplicity to have two variables, $V = \{ x,y \}$. | ||
| ===== Rules for Computing Weakest Preconditions ===== | ===== Rules for Computing Weakest Preconditions ===== | ||
| Line 30: | Line 32: | ||
| x' = e \land y' = y | x' = e \land y' = y | ||
| \] | \] | ||
| - | Then we have | + | Then we have, for formula $Q$ containing $x$ and $y$: |
| \[ | \[ | ||
| \begin{array}{rl} | \begin{array}{rl} | ||
| - | wp(x=e,\{(x,y) \mid Q(x,y)\}) & = \{(x,y) \mid \forall x'.\forall y'.\ x'=e \land y'=y \rightarrow Q(x',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(e,y) \} = \{(x,y) \mid Q[x:=e]\} | + | & = \{(x,y) \mid Q[x:=e] \} |
| \end{array} | \end{array} | ||
| \] | \] | ||
| - | From here we obtain | + | From here we obtain: |
| \[ | \[ | ||
| wp(x = e, Q) = Q[x:=e] | wp(x = e, Q) = Q[x:=e] | ||