Loop invariant is some condition which holds at the end of each iteration of the loop. i.e. it is "invariant" => does not vary (or change). It might change inside one iteration, but it will be true at the end of every iteration.
We often use loop invariants to prove that our algorithm works correctly.
In the given program, a loop invariant is:
i mod 2 = 0
i.e. i is even after every iteration.
One can verify this as follows:
- Before the execution of first iteration the loop invariant is true, because of this line of code:
if i mod 2 = 0 then
- In every iteration, we divide i by $2$, so now i will be either odd or even.
- So, at the end of every iteration i remains even.
https://stackoverflow.com/questions/3221577/what-is-a-loop-invariant