Loop Invariants

I am reading about loop invariants and I don’t understand one thing:

For algorithm

r = c 
while r > 0:
r = 31 * r % 73

Is r < 73 loop invariant?

Answer in the book says yes, but from what I understand loop invariant needs to be true before program enters the loop.
And we can set r to 74 for example so before the loop invariant isn’t true only inside and after the loop it will stay true.

I agree with you. Maybe there’s some mention of c before this? Or maybe it’s just an error in the textbook. All textbooks have errors somewhere.

@andy The loop invariant here is r > 0. Next, the code should be formatted as follows in Python:

r = c
while r > 0:
  r = 31 * r % 73

Note: If c is set to 74, the invariant is true when entering the while loop. For example, 74 > 0 is true.

The key point is to consider the initialization of the variable r. In the given algorithm, r is initially set to c, and the invariant r < 73 holds as long as c < 73. If c is initially less than 73, then r < 73 is indeed a loop invariant because it holds before entering the loop, remains true during each iteration, and after the loop terminates. The book assumes c < 73 for the invariant to be valid throughout. Perhaps that’s the missing context.

1 Like