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 10:31] pedagand |
sav08:hoare_logic [2009/03/04 11:01] 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 37: | Line 38: | ||
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. | + | This is simply relation image of a set. (Note the similarity with relation composition.) |
{{sav08:sp.png?400x250|}} | {{sav08:sp.png?400x250|}} | ||
Line 57: | Line 59: | ||
- $\{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 67: | Line 70: | ||
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 125: | Line 128: | ||
* $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 139: | Line 143: | ||
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 \{ 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}} |