A loop invariant is a set of conditions that are:
- true when the loop is initialized
- maintained in each pass through the loop
- true at termination
Loop invariant arguments are analogous to mathematical induction: they use a base case along with an inductive step to show that the desired proposition is true in all cases.
For example, one feasible loop invariant for the kth largest/smallest algorithm would be the following:
At each iteration, the “active subarray” (call it activeA) consists of all elements of A which are between min(activeA) and max(activeA), and the current index (call it i) has the property that the ith-smallest element of activeA is the ith-smallest element of A.