# 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

A loop invariant is an expression that is true through all iterations. But it should also lead to the post-condition being true when the loop terminates. Although c-a=1 is true, It doesn't help you in achieving the post-condition.

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.

The formal proof should follow from this idea.

Assume $$M$$ and $$N$$ are both non-negative. There are a few invariants for the loop (we can verify them to hold prior to the loop, and after each iteration):

$$P\colon M = aN + b$$

$$Q\colon c-a = 1$$

$$R\colon M-aN \ge 0$$

Note, $$P \land R \Rightarrow b \ge 0$$

The loop's condition is:

$$C\colon M-cN \ge 0$$

$$\Leftrightarrow M-(a+1)N \ge 0$$ {due to $$Q$$}

$$\Leftrightarrow M-aN \ge N$$

Upon termination, $$C$$ is false, so following would hold:

$$M-aN < N$$

$$\Leftrightarrow b < N$$ {due to $$P$$}

Also,

$$b \ge 0$$ {due to $$P \land R$$}

So, $$a$$ and $$b$$ must contain the desired quotient and remainder ($$0 \le b < N$$) such that: $$M = aN + b$$.