LARA

Hoare Logic Rules for Loops

The rule for simple loops is:

\begin{equation*}
\frac{(\models P \rightarrow I);\ \{I\}c\{I\};\ (\models I \rightarrow Q)}
     {\{P\}\ {\it l{}o{}o{}p}\{I\}(c)\ \{Q\}}
\end{equation*}

We can prove that this rule is sound by induction.

Knowing that the while loop:

while (F) c;

is equivalent to:

loop (assume(F); c); 
assume(not F);

Question: What is the rule for while loops?

Hint

Answer