Loop Invariant

Tags

comp-sci

Is a inductive approach to [see page 14, proving] the correctness of algorithms with loops. A loop invariant is a statement that is always true and reflects the progress of the algorithm towards producing a correct output.

The proof process is establishing the invariant is true at:

1. Initialisation: The invariant holds before the algorithm has done anything.
2. Maintenance: Show that if the invariant holds for \( i \) iterations then it also holds after the \( i+1^{\text{th}} \) iteration.
3. Termination When the algorithm terminates the loop invariant tells us that the algorithm is correct.