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