Invariant: say what remains true while the state changes

Replay label: Core Invariant

You can trace an algorithm on three examples and still feel unsure about one update. Should the boundary become mid or mid + 1? Should the current value enter the map before or after the lookup? A useful invariant explains those decisions.

An invariant is a claim about the program’s state at a specified recurring point, usually just before each loop iteration. Variables change, but the relationship the claim describes remains true whenever execution reaches that point.

Think of a librarian moving books from an unsorted cart to a shelf. The particular books on the shelf change. The rule “the shelved books are in alphabetical order” can remain true after every placement. That rule alone does not prove that no book was lost; a stronger argument also accounts for which books have been moved. Algorithmic invariants need the same attention to what the final answer requires.

State a checkpoint, a region, and a claim

“The map is correct” is too vague. “At the start of iteration i, the map contains one earlier index for every distinct value in positions 0 through i - 1, and contains no later indices” can be checked and used.

An invariant often has three ingredients:

• Checkpoint: When is it supposed to hold?
• Region or state: Which indices, entries, nodes, or accumulated values does it describe?
• Meaning: What do those values establish about the work already done or still possible?

Use “before the next iteration” carefully. A multi-statement update may temporarily break the relationship and restore it before the checkpoint. Requiring the invariant to hold after every individual assignment can be stronger than the algorithm needs.

Start from the result you need

Suppose you want the sum of an array. At the end, total should equal the sum of all n elements. Replace “all n” with “the first i” to get a candidate loop invariant:

Before processing index i, total equals the sum of entries with indices smaller than i.

For [4, -2, 7], the checkpoints are:

Next index i	Already processed	total
0	Nothing	0
1	[4]	4
2	[4, -2]	2
3	[4, -2, 7]	9

The final row is the same claim with i = n. That is why this invariant is useful: finishing the loop turns the partial-result statement into the desired complete-result statement.

This construction is not universal, but it is a good starting question: what would a partially completed correct answer mean?

Discharge four obligations

Writing an invariant is a proposal. To use it as a correctness argument, establish four things:

1. Initialization: It is true before the first iteration.
2. Maintenance: If it is true before an iteration and the loop continues, the update makes it true at the next checkpoint.
3. Exit: The invariant together with the stopping condition implies the required result.
4. Progress: The loop cannot continue forever.

The first three establish what happens if the loop terminates. The fourth establishes termination. Cornell’s treatment makes this distinction explicit. Loop invariants

For the sum, initialization uses the empty prefix and zero. Maintenance adds the next element and advances i. Exit gives i = n. Progress follows because the number of unprocessed entries decreases by one per iteration.

Derive binary search’s updates

Consider a sorted ascending array of distinct integers. Return the target’s index if present, or -1 otherwise. Use an inclusive interval: both left and right are candidates.

At each loop checkpoint, maintain:

Every possible occurrence of the target is inside [left, right]; discarded positions cannot contain it. The bounds satisfy 0 ≤ left ≤ right + 1 ≤ n.

This conditional wording matters. “The target is inside the interval” is false when the target never existed. The algorithm must still handle that input.

Initialization. Set left = 0 and right = n - 1. The interval includes the whole array. For an empty array it is already empty, and the bounds still make sense.

Maintenance. While left ≤ right, inspect a midpoint mid inside the interval:

• If numbers[mid] === target, return mid; the returned index directly satisfies the contract.
• If numbers[mid] < target, every position at or left of mid within the interval is too small. Set left = mid + 1.
• If numbers[mid] > target, every position at or right of mid is too large. Set right = mid - 1.

The + 1 and - 1 follow from having inspected and rejected the midpoint. They are not arbitrary details to memorize.

Exit. If the loop ends without a return, left > right. No candidate positions remain. The invariant says discarded positions cannot contain the target, so returning -1 is justified.

Progress. On every nonreturning iteration, the number of candidates, right - left + 1, strictly decreases. It is a nonnegative integer while the loop continues, so the process must stop.

For [1, 3, 5], target 5, the first midpoint is index 1. Its value is too small, so the surviving interval is [2, 2]. The next comparison returns 2. The proof explains why that move is safe for all sorted inputs under this contract, not just this trace.

Other binary-search variants use half-open intervals or seek a boundary rather than an exact match. Their invariants and updates differ. Mixing a loop condition from one variant with an update from another is a common source of errors.

Use an invariant to choose map-update order

For the one-pass Two Sum approach, use two related claims before index i:

1. The map contains one valid earlier index for every distinct value already processed, and no current or future indices.
2. If the function has not returned, no valid pair lies entirely within the processed prefix.

The first claim ensures any successful lookup uses a distinct earlier position. The second explains why you have not missed an answer.

When the complement is present, return its stored earlier index and i. When it is absent, no pair ending at i is possible. Adding the current value then prepares the map for the next iteration. Updating an existing value to its latest index is safe here: any one earlier occurrence is enough when the contract asks for any pair.

If a solution has indices a < b, processing b finds an earlier complementary value unless a solution was already returned. If the scan ends without a match, the whole array has become the processed prefix, so the second claim justifies returning no pair.

Inserting before checking would allow the current entry to supply its own complement. On [3], target 6, that can produce the illegal pair [0, 0]. The update order is a consequence of the invariant and the distinct-index contract.

Avoid invariants that explain too little

Weak claim	What is missing?
“The array is sorted” during binary search	Which remaining interval can still contain the target
“Visited cells have been seen”	What being visited means and whether relevant neighbors are still scheduled
“The prefix is sorted” during sorting	Whether the output retains exactly the required input elements
“The answer is correct so far”	A precise meaning of the partial answer

A claim may be true and still fail to prove the result. Strengthen it by asking what you need at exit.

For island counting, checkpoints between completed floods are especially useful: every land cell already encountered by the outer scan has had its entire component marked, and the count equals the number of components explored so far. Within a flood, use a separate claim: scheduled cells are reachable from the seed, and discovered cells are either pending or already processed. Do not pretend one vague “visited is correct” sentence covers both loops.

Practice the move

A binary-search loop uses while (left < right) but returns -1 immediately after the loop. What happens to [7], target 7?

The loop never runs, even though one candidate remains. The invariant does not imply “not found” at that exit. Either the loop must include the singleton case, or the algorithm needs an explicit final-candidate check consistent with its chosen variant.

An invariant is not a hypothesis that becomes proven merely by surviving tests. It is a claim whose initialization, preservation, exit consequence, and progress you must justify. Use tests and traces to challenge the argument and its implementation.

Where to