Proving Algorithm Correctness with Invariants

Welcome back. In the previous lesson, you practiced breaking tempting claims with minimal counterexamples. That is the right first defense against an unproved algorithmic idea. But surviving targeted attacks is not a proof. Once an iterative idea looks plausible, you need a compact statement that records what every completed step has made permanently true.

That statement is a loop invariant. In competitive programming, it is often the difference between “this simulation feels right” and a solution sketch you can trust before investing time in implementation.

By the end of this lesson, you should be able to state an invariant for a scan or constructive process, check that it starts true and stays true, and use the loop’s stopping condition to derive exactly what the algorithm promises.

---

The contract at a loop boundary

A loop invariant is a logical statement that is true:

• after initialization, just before the first guard check;
• at the beginning of every later iteration;
• when the loop exits.

The important location is the loop boundary: the moment just before evaluating the guard. An invariant is not merely a fact that happens to be true somewhere in the loop body.

Suppose an algorithm has:

• a precondition $Q$, describing valid inputs;
• initialization;
• a loop guard $G$;
• loop body $S$;
• a required postcondition $R$.

A useful invariant $P$ supports a correctness argument through three linked claims:

1. Initialization: after setup, $P$ holds.
2. Maintenance: if $P$ holds and the guard $G$ is true, one execution of $S$ restores $P$.
3. Termination use: when the loop stops, $P$ together with the false guard establishes $R$.

The first two claims mean that $P$ remains true throughout execution. The third is where the invariant earns its place: it translates the final program state into the required answer.

A fourth question is needed for total correctness:

4. Progress: why does the loop actually terminate?

An invariant alone proves partial correctness: if the loop ends, its answer is correct. A progress argument rules out an infinite loop. Typical progress measures are an index moving toward $n$, a remaining interval shrinking, or a nonnegative quantity decreasing.

A statement can be technically invariant yet useless. For example, $1=1$ remains true in every loop, but it says nothing about the answer. Likewise, “the array exists” may remain true, but it cannot establish that you found a target, constructed a valid object, or optimized a quantity.

The right question is not:

What remains unchanged?

It is:

What exact knowledge about the partial computation remains true, and what will that knowledge imply when no work remains?

---

A reliable method for discovering the invariant

For most contest loops, begin with the boundary between what has been settled and what remains unresolved. If an index $i$ advances left to right, then at the start of an iteration it commonly separates:

• the processed prefix $a[0\dots i-1]$, and
• the unprocessed suffix $a[i\dots n-1]$.

Then ask what the maintained variables mean exactly for that processed region.

Common invariant patterns are:

Loop purpose	Typical invariant shape
Scanning an array	An accumulator gives the correct summary of the processed prefix.
Searching	Every eliminated position is impossible; every remaining position is still a candidate.
Partitioning / two pointers	Elements on each side of the boundaries satisfy their required classification.
Constructing an object	The partial object is valid, and processed items have been handled in a way that supports the final specification.
Transforming quantities	A conserved expression involving the current variables equals its original value.

A practical derivation routine is:

1. Write the final requirement. What must be true at the end?
2. Replace “the whole input” with “the processed part.” This often produces a first invariant candidate.
3. State what each variable represents. Avoid vague phrases such as “best so far” unless you specify best among which objects.
4. Add bounds and feasibility facts. For example, $0\le i\le n$, or “the chosen vertices are independent.”
5. Mentally substitute the exit condition. If the result does not become the desired final statement, strengthen or redesign the invariant.

Cornell’s Correctness Issues and Loop Invariants develops this process using a summation loop, then generalizes it to prefix processing.

The phrase “processed prefix” is not itself an invariant. You must say what is true of it. For example:

• “sum equals the sum of all values in the processed prefix.”
• “best is the maximum value in the processed prefix.”
• “No processed position contains the target.”
• “The constructed answer uses only processed items and satisfies all local constraints.”

---

Worked example: two linked invariants in Kadane’s algorithm

Consider the maximum subarray sum problem for a nonempty array $a$. Kadane’s algorithm is often remembered as two assignments:

long long end_here = a[0];
long long best = a[0];

for (int i = 1; i < n; i++) {
    end_here = max(a[i], end_here + a[i]);
    best = max(best, end_here);
}

Memorizing those lines is fragile. The invariant explains them.

At the start of an iteration with index $i$, where $1\le i\le n$, state both facts:

$$\text{end\_here}=\max \{\text{sum of a nonempty subarray ending at }i-1\}$$

and

$$\text{best}=\max \{\text{sum of a nonempty subarray contained in }a[0\dots i-1]\}.$$

These facts have distinct jobs:

• end_here summarizes the best subarray that can be extended by $a_i$.
• best summarizes the best complete answer encountered anywhere in the processed prefix.

Initialization

Before the first iteration, $i=1$. The processed prefix contains only $a_0$.

• The best nonempty subarray ending at index $0$ is $[0,0]$, with sum $a_0$.
• The best nonempty subarray anywhere in the one-element prefix is also $[0,0]$.

So both variables initialized to $a_0$ make the invariant true.

Maintenance

Assume the invariant holds at the start of iteration $i$. Any nonempty subarray ending at $i$ has only two possible forms:

1. It consists solely of $a_i$.
2. It is a subarray ending at $i-1$, extended by $a_i$.

Among all possibilities of the second form, the best predecessor is exactly the quantity stored in end_here by the invariant. Therefore:

$$\max \{\text{sum of a nonempty subarray ending at }i\}=\max (a_i,\text{end\_here}+a_i).$$

The first assignment restores the meaning of end_here for the larger prefix.

Now consider the overall optimum within $a[0\dots i]$. It is either:

• the old optimum in $a[0\dots i-1]$, stored in best; or
• a subarray that ends at $i$, whose optimum is the newly updated end_here.

Thus the second assignment restores the meaning of best.

Termination and progress

The loop ends after $i=n$. The invariant then says best is the maximum subarray sum within $a[0\dots n-1]$, which is precisely the required answer.

Progress is immediate: $i$ increases once per iteration and cannot exceed $n$.

The key lesson is that an invariant may contain several coupled facts. A weak statement such as “best is large” cannot justify the transition. The exact semantics of end_here explain why extending only one prior value is sufficient.

---

Constructive algorithms: validity is not the same as optimality

In a constructive algorithm, the invariant usually has two layers:

1. the object built so far is valid;
2. every processed item has been dealt with in a way that establishes the actual final guarantee.

Consider a graph $G$ with vertices processed in a fixed order. This greedy algorithm constructs an independent set:

S = empty set

for each vertex v in the chosen order:
    if no neighbor of v belongs to S:
        add v to S

At the start of the iteration for vertex $v_i$, let the preceding vertices be $v_0,\dots ,v_{i-1}$. A strong invariant is:

1. $S$ is an independent set.
2. Every processed vertex either belongs to $S$ or has a neighbor in $S$.

The first property gives feasibility. The second records the consequence of every rejection.

Why it starts and stays true

Initially, $S$ is empty and no vertices have been processed, so both statements hold.

During an iteration:

• If the algorithm adds $v_i$, its test guarantees it has no neighbor already in $S$. Therefore $S$ remains independent. The newly processed vertex satisfies the second condition because it belongs to $S$.
• If the algorithm skips $v_i$, the test found a neighbor already in $S$. So the second condition becomes true for $v_i$, while neither property is damaged for earlier vertices.

At termination, every vertex has been processed. Thus every vertex outside $S$ has a neighbor in $S$. No outside vertex can be added while preserving independence, so $S$ is a maximal independent set.

That is a complete proof of the claim “return a maximal independent set.”

It is not a proof that $S$ has maximum possible size. On a star graph, process the center first. The algorithm selects the center and rejects every leaf, returning a set of size $1$. Selecting all leaves gives a larger independent set.

This distinction should be automatic in contest reasoning:

• valid: the object obeys the constraints;
• maximal: no single allowed extension can be added;
• maximum: no valid solution has a better objective value.

An invariant proves only what it actually states. If the problem demands an optimum, an invariant that establishes merely validity or maximality is insufficient. This is exactly the logical discipline behind the counterexamples from the previous lesson.

---

A contest-ready invariant checklist

Before coding a loop or construction, write a two- or three-line proof sketch:

Invariant at the loop head:
[exact meaning of state variables for the processed region]
[feasibility / partition / elimination property]

Maintenance:
[why this iteration updates the state without violating that meaning]

Exit:
[substitute the stopping condition and obtain the required result]

Progress:
[state the bounded quantity that moves toward termination]

Use especially careful wording around indices:

• Is $i$ the last processed position or the first unprocessed one?
• Does your range include $i$ or exclude it?
• Is the invariant meant to hold before the body, after the body, or both at the next loop boundary?
• If the loop can return early, have you separately justified that return path?

For a proposed invariant, two rapid checks often expose flaws before coding:

• Initialization check: Substitute the initial values literally. Empty prefixes and empty constructions should make sense.
• One-iteration check: Assume only the invariant and the guard. Do not rely on vague memories of earlier iterations; every relevant fact about the past must already be encoded in the invariant.

---

Takeaways

A loop invariant is a precise statement about the program state that holds at every loop boundary. To use one for correctness:

• establish it after initialization;
• show one legal iteration preserves it;
• combine it with the false loop guard at exit to derive the postcondition;
• separately show progress toward termination.

For array scans, the most common form is “the variables summarize the processed prefix exactly.” For constructive algorithms, include both the validity of the partial construction and the fate of processed items. Most importantly, match the invariant to the claim you need: proving a construction is valid or maximal does not prove it is optimal.

Next, you will use the closely related idea of induction to prove recursive and recurrence-based algorithms correct.