# Loop termination - Loop invariant

(x >= 0 && y >= 0)
q = 0;
r = x;
while ( r >=y ) {
r = r - y;
q = q + 1;
}
(x = q*y +r) && (r >= 0) && (r < y)


For this what if y = 0 ?

If y = 0, then r stays at r inside the while loop, which makes r >= y true always. So it doesn't seem to terminate.

So I think, for pre-condition, doesn't it have to be (y > 0) to make sure this program terminates ?

• Could you add if & while clauses to the first and last statements? It's a bit confusing. Apr 22, 2018 at 5:58
• If $y=0$ then the loop never terminates. Depending on your semantics of Hoare triples, either this is OK (the loop never terminates, so the postcondition is never falsified) or not (your precondition must ensure that the code terminates). But it just seems like a typo for $y>0$. Apr 22, 2018 at 6:07
• To clarify: Are these partial correctness assertions (typically written with {}) or total correctness assertions (typically written with [])? If they are partial correctness assertions, they don't require the loop terminates; they only describe what needs to happen when it does determine. Apr 22, 2018 at 6:20

The Hoare logic rules for program statements are roughly the same, except for while loops. In partial correctness, the while rule requires to find a suitable invariant property. In total correctness, the rule requires both the invariant property and the variant: this is a strictly decreasing, natural valued function of the state (roughly, providing an upper bound on the number of loops).