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