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 [2009/02/25 14:34] vkuncak |
sav08:hoare_logic [2009/02/25 14:34] vkuncak |
||
|---|---|---|---|
| Line 141: | 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 ===== | ===== Composing Hoare Triples ===== | ||
| Line 146: | Line 147: | ||
| \[ | \[ | ||
| \frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} } | \frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} } | ||
| - | { \{P\} c_1 ; c_2 \{ Q \} } | + | { \{P\} c_1 ; c_2 \{ R \} } |
| \] | \] | ||