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