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:hoare_logic [2008/02/29 19:20] vkuncak |
sav08:hoare_logic [2008/03/03 10:31] pedagand |
||
---|---|---|---|
Line 21: | Line 21: | ||
{r = x * y} | {r = x * y} | ||
</code> | </code> | ||
+ | |||
===== Hoare Triple for Sets and Relations ===== | ===== Hoare Triple for Sets and Relations ===== | ||
Line 31: | Line 32: | ||
means | means | ||
\[ | \[ | ||
- | \forall s,s' \in S. s \in S \land (s,s') \in r \rightarrow s' \in Q | + | \forall s,s' \in S. s \in P \land (s,s') \in r \rightarrow s' \in Q |
\] | \] | ||
We call $P$ precondition and $Q$ postcondition. | We call $P$ precondition and $Q$ postcondition. | ||
Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically, a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas a weaker condition $x > 0$ denotes the entire half-plane.) | Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically, a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas a weaker condition $x > 0$ denotes the entire half-plane.) | ||
+ | |||
Line 47: | Line 49: | ||
Note the similarity with relation composition. | Note the similarity with relation composition. | ||
- | FIXME Graphical illustration. | + | {{sav08:sp.png?400x250|}} |
==== Lemma: Characterization of sp ==== | ==== Lemma: Characterization of sp ==== | ||
Line 54: | 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 64: | 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 ==== |