Loops & Invariants

Loop invariants turn a repeating block into a proof you can inspect. A maximum scan keeps one precise promise at every loop head: best equals the maximum of the processed prefix values[0:i]. Watch that prefix grow and you can see initialization establish the promise, each iteration restore it, and termination turn it into the final answer.

The promise is tied to a checkpoint, not vaguely to the whole loop. Here that checkpoint is the moment just before Python tests i < len(values). The loop body may temporarily move from the old prefix toward the next one; it must restore the promise before control returns to the checkpoint.

Reach for an invariant when a loop boundary is easy to get wrong: binary search, a two-pointer scan, or an unfamiliar while loop. State what the processed region guarantees at the loop head. The first checkpoint that fails tells you where the bug entered.

How loop invariants work

A useful loop invariant has three jobs.

1. Initialization: prove the promise before the first condition check.
2. Maintenance: assume the promise at one loop head, run one iteration, and prove it again at the next loop head.
3. Termination: combine the promise with the false loop condition to derive the final result.

For the maximum scan, the invariant is best = max(values[0:i]). The slice ends before i, so it contains exactly the values already processed. Initializing best = values[0] and i = 1 makes the first prefix [values[0]]; its maximum is plainly values[0].

During an iteration, values[i] is the one unprocessed candidate entering the proof. The assignment best = max(best, values[i]) establishes best = max(values[0:i + 1]). Then i = i + 1 changes the name of that same boundary, restoring the loop-head form best = max(values[0:i]).

Loops and invariants step by step

The default run uses values = [3, 1, 4, 2, 5].

1. Line 1 sets best = 3. Line 2 sets i = 1. The processed prefix is [3], so the invariant holds before the first check.
2. The condition 1 < 5 is true. The candidate is values[1] = 1; max(3, 1) leaves best = 3. Incrementing i to 2 restores the invariant for [3, 1].
3. The condition 2 < 5 is true. The candidate is 4, so best becomes 4. With i = 3, the processed prefix is [3, 1, 4] and its maximum is 4.
4. The condition 3 < 5 is true. The candidate is 2, so best stays 4. Incrementing i to 4 extends the proved prefix through index 3.
5. The condition 4 < 5 is true. The candidate is 5, so best becomes 5. Incrementing i to 5 makes the processed prefix the whole list.
6. The condition 5 < 5 is false. The loop stops, and line 6 prints 5.
7. Now change only line 1 to best = 0 and use [-8, -3, -11, -2, -5]. At the first checkpoint, 0 ≠ max([-8]) = -8, so the proof never gets established.
8. Every candidate is negative, so best stays 0. The program prints 0 even though the list's true maximum is -2.

The moving bracket is the loop-head proof boundary. During inspection and maintenance, the candidate stays outside the bracket even after best has absorbed it. That gap is deliberate: advancing i moves the bracket and restores the exact loop-head formula.

Why the initializer can break the proof

The wrong initializer exposes why a plausible-looking loop is not enough. With best = 0 and an all-negative list, the value 0 comes from outside the input and already exceeds every legal candidate. The invariant is false at the first loop head, every update keeps 0, and the program prints a value that never appeared in the list.

Why termination finishes the proof

When the loop stops, i < len(values) is false. The loop only increments i by one and never passes the length, so the stopping state has i = len(values). Substitute that equality into the invariant:

best = max(values[0:i]) = max(values[0:len(values)]).

The second slice is the whole list. The program can print best because initialization and maintenance have already proved what it represents; the false condition supplies the final boundary.

Time and space complexity

For a non-empty list of length n, the loop inspects n - 1 candidates after using the first value to initialize best. Each iteration does constant work, so the running time is O(n). The scan stores only best, i, and a temporary candidate regardless of input size, so its extra space is O(1).

Edge cases

• Singleton list: initialization already covers the whole list. The condition is false immediately, the body runs zero times, and the sole value is printed.
• Empty list: values[0] raises IndexError. This implementation requires at least one value; the empty-input sandbox makes that precondition visible instead of inventing a sentinel.
• All-negative values: initializing from the first element still works. Initializing to 0 does not.
• Duplicate maxima: the invariant concerns the maximum value, so seeing the same maximum again leaves best unchanged without weakening the proof.
• Maximum at the end: the last body iteration must still restore the invariant before the final false check.

Common mistakes

• Saying the invariant holds after every statement. During maintenance, the proof is deliberately written for i + 1 until the increment restores the loop-head form.
• Choosing best = 0 without proving that every input is non-negative. A convenient sentinel can silently change the problem.
• Incrementing i before reading values[i]. That skips a candidate and may read past the end.
• Proving initialization and maintenance but stopping before the termination argument. An invariant only becomes the postcondition when the exit state makes its prefix cover the whole input.
• Testing a few outputs and calling that a proof. Examples can find counterexamples; the three invariant obligations cover every valid input.

A note on simplification

The animation highlights one Python statement at a time. Line 4 takes two beats: it evaluates max(best, values[i]), then writes best. A real interpreter performs smaller operations and manages objects, frames, and exceptions that are outside this lesson. The proof assumes a finite, non-empty sequence of comparable values and ordinary integer indexing; concurrent mutation and custom comparison behavior are not modeled.