---
title: "Loops & Invariants"
description: "Loop variables, the invariant that holds each pass, and the termination condition."
source: https://vizlearn.app/foundations/execution-model/loops-invariants
---

# 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.