Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:hoare_logic [2008/03/03 10:31] pedagand |
sav08:hoare_logic [2008/03/03 10:31] pedagand |
||
|---|---|---|---|
| Line 57: | Line 57: | ||
| - $\{P\} r \{ sp(P,r) \}$ | - $\{P\} r \{ sp(P,r) \}$ | ||
| - $\forall Q \subseteq S.\ \{P\} r \{Q\} \rightarrow sp(P,r) \subseteq Q$ | - $\forall Q \subseteq S.\ \{P\} r \{Q\} \rightarrow sp(P,r) \subseteq Q$ | ||
| + | |||
| ===== Weakest Precondition - wp ===== | ===== Weakest Precondition - wp ===== | ||
| Line 67: | Line 68: | ||
| Note that this is in general not the same as $sp(Q,r^{-1})$ when relation is non-deterministic. | Note that this is in general not the same as $sp(Q,r^{-1})$ when relation is non-deterministic. | ||
| - | FIXME Graphical illustration. | + | {{sav08:wp.png?400x250|}} |
| ==== Lemma: Characterization of wp ==== | ==== Lemma: Characterization of wp ==== | ||