Loop invariants
A fact that is true every time control is at the top of the loop.
It is true before the first iteration, between iterations, and when the loop condition has just failed. It is a comment you prove. It does not execute.
Phil wakes up to the same song and the day resets. What he is allowed to carry is the invariant: a fact that is still true at the top, no matter which copy of the day this is. Initialization is the first morning. Maintenance is one day that preserves the fact. Termination is what you can conclude once the loop stops.
- Initialization. True before iteration one. Often an empty range, a one-element range, or a variable that is still 0.
- Maintenance. Assume it at the start of an arbitrary iteration. Show it at the start of the next one. This is induction. You must use the assumption, not the thing you are still proving.
- Termination. The invariant is still true, and the loop test is now false. Name the counter’s exact value. Deduce the goal. This part is not induction.
How to invent one
At the top of the loop, with the counter sitting on \(j\), what useful fact is already true about the work finished so far? Finished almost always means the indices strictly before \(j\).
| The loop’s job | Shape that usually works |
|---|---|
| Sum or product | \(s\) equals the sum or product of \(A[0..j-1]\) |
| Count | count equals how many of \(A[0..j-1]\) passed the test |
| Max or min | \(m\) equals the max or min of \(A[0..j-1]\) |
| Search | found is true exactly when the needle is in the prefix |
| Insertion sort | the prefix is the original prefix, sorted |
| Selection sort | the prefix is the smallest so far, sorted, and ≤ the suffix |
Then plug in the first value of the counter. If the claim becomes awkward or false, the range is off by one. Fix the range before you write a long maintenance paragraph.
“Every dragon in this closet is house-trained” is true when the closet is empty, because there is no dragon available to be a counterexample. An empty prefix is sorted. Selection sort’s invariant at \(k = 0\) is that sentence.
Model proof: the product that becomes \(N!\)
p = 1
i = 1
while (i <= N)
p = p * i
i = i + 1
Invariant. At the top of the loop, \(p = (i-1)!\). The empty product is 1.
Initialization. \(i = 1\) and \(p = 1\). That is \(0!\). Holds.
Maintenance. Assume \(p = (i-1)!\) and that the body runs, so \(i \le N\). After p = p * i, \(p = i!\). Then \(i\) becomes \(i+1\). Relative to the new counter, \(p = (i'-1)!\).
Termination. \(i\) starts at 1 and increases by exactly 1, so the first time \(i \le N\) fails we have \(i = N+1\) (for \(N \ge 1\)). Then \(p = N!\). If \(N = 0\), the test fails immediately and \(p = 1 = 0!\).
A paragraph you can imitate
Assume that at the start of iteration \(j\), the invariant holds for this \(j\). The body does one concrete thing to the tracked variables. Afterward, write the new equation. Because \(j\) becomes \(j+1\), that equation is the invariant for the next test.
Try this
The loop should leave \(m\) equal to the maximum of \(A[0..N-1]\), assuming \(N \ge 1\).
m = A[0]
j = 1
while (j < N)
if (A[j] > m) m = A[j]
j = j + 1
Show the invariant and the three steps
Invariant. \(m = \max(A[0..j-1])\).
Initialization. \(j = 1\), so the range is \(A[0..0]\), and \(m = A[0]\).
Maintenance. Assume \(m\) is the max of \(A[0..j-1]\). The if sets \(m\) to \(A[j]\) when \(A[j]\) is larger, and leaves \(m\) alone otherwise. Either way, \(m\) becomes the max of \(A[0..j]\). Then \(j\) increases by 1.
Termination. \(j\) increases by 1 from 1, so exit is exactly \(j = N\). Then \(m = \max(A[0..N-1])\).
The if does not change how many times the loop runs. This scan is \(\Theta(N)\) on every input of length \(N\).