• English only

# 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] (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 ?);\ \{?​\}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*}
++++ ++++

-$+\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*}