3
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ $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. $\endgroup$ – David Richerby May 9 '17 at 9:49
  • $\begingroup$ 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. $\endgroup$ – chi May 10 '17 at 16:38
8
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.