A statement that is true upon entering the loop, and after every iteration. Used after loop exit to prove that the algorithm is correct. Ideally tries to include 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