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:43] vkuncak |
sav08:backward_vcg [2015/04/21 17:30] (current) |
||
---|---|---|---|
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 ===== | ||
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 12: | 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 18: | 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 | + | Then we have, for formula $Q$ containing $x$ and $y$: |
- | \[ | + | \begin{equation*} |
\begin{array}{rl} | \begin{array}{rl} | ||
- | wp(x=e,\{(x,y) \mid Q(x,y)\}) & = \{(x,y) \mid \forall x',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} | ||
- | \] | + | \end{equation*} |
- | From here we obtain | + | 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 ===== |