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:35] 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. | ||
+ | |||
Line 149: | Line 150: | ||
{ \{P\} c_1 ; c_2 \{ R \} } | { \{P\} c_1 ; c_2 \{ R \} } | ||
\] | \] | ||
+ | |||
+ | We can prove this from | ||
+ | * definition of Hoare triple | ||
+ | * meaning of ';' as $\circ$ | ||
===== Further reading ===== | ===== Further reading ===== | ||
* {{sav08:backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}} | * {{sav08:backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}} |