# Hoare Logic Rules for Loops

The rule for simple loops is:

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

It follows that the rule for while loops is: