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
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?