Differences
This shows you the differences between two versions of the page.
sav08:hoare_logic_rule_for_loops [2008/03/04 20:33] vkuncak |
sav08:hoare_logic_rule_for_loops [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Hoare Logic Rule for Loops ====== | ||
- | The rule for simple loops is: | ||
- | |||
- | \[ | ||
- | \frac{(\models P \rightarrow I);\ \{I\}c\{I\};\ (\models I \rightarrow Q)} | ||
- | {\{P\}\ {\it l{}o{}o{}p}\{I\}(c)\ \{Q\}} | ||
- | \] | ||
- | |||
- | We can prove that this rule is sound by induction. | ||
- | |||
- | Knowing that the while loop: | ||
- | |||
- | <code> | ||
- | while (F) c; | ||
- | </code> | ||
- | |||
- | is equivalent with: | ||
- | |||
- | <code> | ||
- | loop (assume(F); c); | ||
- | assume(\lnot F); | ||
- | </code> | ||
- | |||
- | **Question:** What is the rule for while loops? | ||
- | ++++Hint| | ||
- | \[ | ||
- | \frac{(\models P \rightarrow ?);\ \{?\}c\{?\};\ (\models ? \rightarrow Q)} | ||
- | {\{P\}\ {\it while}\{I\}(F)(c)\ \{Q\}} | ||
- | \] | ||
- | ++++ | ||
- | |||
- | ++++Answer| | ||
- | It follows that the rule for while loops is: | ||
- | \[ | ||
- | \frac{(\models P \rightarrow I);\ \{I \wedge F \}c\{I\};\ (\models (I \land \lnot F) \rightarrow Q))} | ||
- | {\{P\}\ {\it while}\{I\}(F)(c)\ \{Q\}} | ||
- | \] | ||
- | ++++ |