This is an old revision of the document!

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:

while (F) c;

is equivalent with:

loop (assume(F); c); 
assume(\lnot F);

Question: What is the rule for while loops?

\[ \frac{(\models P \rightarrow ?);\ \{?\}c\{?\};\ (\models ? \rightarrow Q)}

   {\{P\}\ {\it while}\{I\}(F)(c)\ \{Q\}}

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\}}