A statement that is true upon entering the loop, and after every iteration. Used after loop exit to prove that the algorithm is correct. A good loop invariant includes:
- All relevant variables required in the final proving statement.
Proving Loop Invariance
Basis
Show that LI holds when entering the loop
Induction Step
- Consider arbitrary iteration of the loop
- Suppose LI holds before iteration (IH)
- WTP LI holds after iteration