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?