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/03/03 09:44] pedagand |
sav08:hoare_logic [2009/02/25 14:34] vkuncak |
||
|---|---|---|---|
| Line 37: | Line 37: | ||
| 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 48: | 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 55: | 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 65: | 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 ==== | ||
| Line 123: | Line 126: | ||
| * $sp(P,r) \subseteq Q$ | * $sp(P,r) \subseteq Q$ | ||
| + | |||
| ===== Hoare Triples, Preconditions, Postconditions on Formulas and Commands ===== | ===== Hoare Triples, Preconditions, Postconditions on Formulas and Commands ===== | ||
| Line 137: | Line 141: | ||
| We then similarly extend the notion of $sp(P,r)$ and $wp(r,Q)$ to work on formulas and commands. We use the same notation and infer from the context whether we are dealing with sets and relations or formulas and commands. | We then similarly extend the notion of $sp(P,r)$ and $wp(r,Q)$ to work on formulas and commands. We use the same notation and infer from the context whether we are dealing with sets and relations or formulas and commands. | ||
| + | |||
| + | ===== Composing Hoare Triples ===== | ||
| + | |||
| + | \[ | ||
| + | \frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} } | ||
| + | { \{P\} c_1 ; c_2 \{ Q \} } | ||
| + | \] | ||
| ===== Further reading ===== | ===== Further reading ===== | ||
| * {{sav08:backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}} | * {{sav08:backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}} | ||