# Loop invariant for a division algorithm

I'm having problems trying to understand the concept of loop invariants.

I have the following code, where M and N are predefined constants.

a = 0
b = M
c = 1
while M - c * N >= 0:
a = c
c = c + 1
b = M - a * N
print(a, b)


I have figured out this code is actually a division algorithm, where in the end prints out a as the quotient of M/N and b as the remainder. But it's unclear to me what the invariant here is. Can I say c-a is the invariant since c-a=1 is always true before and after every iteration? How could I prove that in a mathematical perspective?

• $c-a$ certainly is an invariant, but it doesn't look like a very useful one, since the algorithm could easily be rewritten to use only $c$, and the fact that $c-a=1$ after each iteration doesn't really help you determine what the algorithm does. – David Richerby May 9 '17 at 9:49
• Start by writing a formal postcondition in terms of $a,b$, preferably involving multiplication instead of quotient & remainder. Then try to modify that to involve $c$ as well, so that it is also true in the intermediate iterations. – chi May 10 '17 at 16:38

Intuitively, You would want the invariant to be a*N + b = M because that's what division is and that's what guarantees that you'll get the post-condition ( a=quotient, b=remainder) when the termination condition ( b < N ) is true.