Loop invariant for a division algorithm

Question

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?

Answer 1

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.

Answer 2

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$.