Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:backward_vcg [2008/03/04 22:30] vkuncak |
sav08:backward_vcg [2009/03/12 12:43] vkuncak |
||
---|---|---|---|
Line 14: | Line 14: | ||
\[ | \[ | ||
\begin{array}{rl} | \begin{array}{rl} | ||
- | wp(\Delta_A,Q) & = \{x \mid \forall x'. (x,x') \in \Delta_A \rightarrow x' \in Q \} \\ | + | wp(\Delta_F,Q) & = \{s \mid \forall s'. (s,s') \in \Delta_F \rightarrow s' \in Q \} \\ |
- | & = \{ x \mid \forall x'. (x \in A \land x=x') \rightarrow x' \in Q \} \\ | + | & = \{ s \mid \forall s'. (s \in F \land s=s') \rightarrow s' \in Q \} \\ |
- | & = \{ x \mid x \in A \rightarrow x \in Q \} | + | & = \{ s \mid s \in F \rightarrow s \in Q \} |
\end{array} | \end{array} | ||
\] | \] | ||
- | Putting $A = \{x\mid F(x)\}$ we obtain the rule on formulas: | + | 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) | wp(assume(F), Q) = (F \rightarrow Q) |