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 [2009/02/25 14:34] vkuncak |
sav08:hoare_logic [2009/02/25 14:46] vkuncak |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler. | Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler. | ||
| + | |||
| ===== Example Proof ===== | ===== Example Proof ===== | ||
| - | <code> | + | <code java> |
| - | {0 <= y} | + | //{0 <= y} |
| i = y; | i = y; | ||
| - | {0 <= y & i = y} | + | //{0 <= y & i = y} |
| r = 0; | r = 0; | ||
| - | {0 <= y & i = y & r = 0} | + | //{0 <= y & i = y & r = 0} |
| - | while {r = (y-i)*x & 0 <= i} | + | while //{r = (y-i)*x & 0 <= i} |
| (i > 0) ( | (i > 0) ( | ||
| - | {r = (y-i)*x & 0 < i} | + | //{r = (y-i)*x & 0 < i} |
| r = r + x; | r = r + x; | ||
| - | {r = (y-i+1)*x & 0 < i} | + | //{r = (y-i+1)*x & 0 < i} |
| i = i - 1 | i = i - 1 | ||
| - | {r = (y-i)*x & 0 <= i} | + | //{r = (y-i)*x & 0 <= i} |
| ) | ) | ||
| - | {r = x * y} | + | //{r = x * y} |
| </code> | </code> | ||
| Line 141: | Line 142: | ||
| 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 151: | ||
| { \{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}} | ||