Algorithm Correctness, Invariants & Termination

An algorithm is not correct by resemblance to pseudocode or by passing a large test suite. It is correct with respect to a specification and an execution model: every allowed initial state must lead only to allowed behavior, and, when termination is required, must eventually produce an allowed final state. Invariants make that global claim tractable by exposing facts that survive each local step.

Correctness is a relation, not a property of code alone #

Let $C$ be a command, $P$ a predicate over initial states, and $Q$ a predicate over final states. The Hoare triple

$$\{P\}\;C\;\{Q\}$$

states a conditional guarantee: if execution starts in a state satisfying $P$, then every terminating execution of $C$ ends in a state satisfying $Q$. This is partial correctness. It deliberately says nothing about whether an execution terminates.

Total correctness is partial correctness plus termination from every state satisfying $P$. Keeping those claims separate is useful: the functional argument and the progress argument usually need different evidence.

The precondition is not input validation performed by the proof. It defines the set of calls covered by the theorem; deciding where to enforce it is a separate contract-boundary question. A precondition of false makes any triple vacuously true, and a postcondition of true proves nothing useful. A proof is only as valuable as its contract.

The small calculus behind the proof #

Hoare logic replaces execution of arbitrarily long traces with rules for language constructs. If the rules are sound for the chosen semantics, a derivation built from them covers every trace admitted by that semantics.

In $Q[E/x]$, substitution is logical, not textual search-and-replace: bound variables must be renamed to avoid capture, and the expression must have the language-defined meaning it will have at runtime. Aliasing and heap mutation require assertions over locations or an abstract heap, not only scalar variables.

The loop rule gives

$$\frac{\{I \land B\}\;S\;\{I\}} {\{I\}\;\mathbf{while}\ B\ \mathbf{do}\ S\;\{I \land \neg B\}}.$$

It is a partial-correctness rule. The conclusion says what follows if the loop exits; a separate variant proves that it must exit.

A loop invariant is an induction hypothesis #

An invariant is a predicate over program state that holds immediately before each evaluation of the loop guard. It need not describe a quantity whose numeric value is unchanged. Variables may all change while a relation among them remains true.

For

initialize
while B:
    body

the complete functional argument has three obligations:

1. Initialization: the precondition and initialization imply $I$.
2. Preservation: assuming $I \land B$, one execution of the body re-establishes $I$.
3. Exit: $I \land \neg B$ implies the postcondition.

This is mathematical induction over the number of completed iterations. Initialization is the base case; preservation is the induction step. The exit condition converts the persistent fact into the desired result.

Assertions form an implication order. A stronger assertion describes fewer states. Strengthening an invariant may make the exit proof easier but initialization or preservation harder; weakening it has the opposite effect. Invariant discovery is the search for a predicate that satisfies all three constraints simultaneously.

Worked proof: lower bound in a sorted array #

For a nondecreasing array a and comparable value x, lower_bound returns the first position whose element is not less than x, or len(a) if there is none. The proof assumes that < induces the ordering used to establish the array's sortedness; values such as unordered floating-point NaNs fall outside that precondition.

def lower_bound(a, x):
    lo, hi = 0, len(a)
    while lo < hi:
        mid = lo + (hi - lo) // 2
        if a[mid] < x:
            lo = mid + 1
        else:
            hi = mid
    return lo

Let $n = \lvert a\rvert$. The postcondition for returned position $p$ is

$$0 \le p \le n, \qquad \forall j \in [0,p): a[j] < x, \qquad \forall j \in [p,n): a[j] \ge x.$$

The useful invariant is the same partition with an unresolved interval:

$$0 \le lo \le hi \le n,$$

$$\forall j \in [0,lo): a[j] < x, \qquad \forall j \in [hi,n): a[j] \ge x.$$

The interval $[lo,hi)$ contains precisely the positions not yet classified.

Initialization. lo = 0 and hi = n establish the bounds. Both classified ranges are empty, so their universal statements are vacuously true.

Safe midpoint. The guard gives $lo < hi$. Therefore

$$lo \le mid = lo + \left\lfloor\frac{hi-lo}{2}\right\rfloor < hi,$$

so a[mid] is in bounds. The written form also avoids adding lo + hi; for a fixed-width implementation, the proof must additionally establish that every intermediate arithmetic operation is representable in its actual integer type.

Preservation, left case. If $a[mid] < x$, sortedness gives $a[j] \le a[mid] < x$ for every $j \le mid$. Assigning lo = mid + 1 therefore extends the known-left range without invalidating the right range.

Preservation, right case. Otherwise $a[mid] \ge x$. Sortedness gives $a[j] \ge a[mid] \ge x$ for every $j \ge mid$. Assigning hi = mid extends the known-right range without invalidating the left range.

Exit. The negated guard gives $lo \ge hi$, while the invariant gives $lo \le hi$, hence $lo = hi$. The unresolved interval is empty, and substituting $p=lo=hi$ into the two classified ranges gives the postcondition.

This proof also exposes why several plausible variants are wrong. Updating lo = mid can leave a one-element interval unchanged. Using a closed interval without changing the postcondition alters the midpoint bounds and exit argument. Binary-search bugs are usually representation mismatches among interval convention, updates, and postcondition—not mysterious arithmetic accidents.

Termination needs a well-founded descent #

A value merely “getting smaller” is insufficient: integers can decrease forever. A termination argument maps each state to a well-founded set, one with no infinite descending chain, and proves a strict descent on every continuing step.

For the lower-bound loop, choose the natural-number variant

$$V = hi - lo.$$

The invariant proves $V \ge 0$. Under the guard, $mid \in [lo,hi)$:

• after lo = mid + 1, $V' = hi-mid-1 < hi-lo$;
• after hi = mid, $V' = mid-lo < hi-lo$.

No infinite strictly descending sequence of natural numbers exists, so the loop terminates. Together with the functional argument, this establishes total correctness.

Natural numbers are only the simplest ranking domain. Structural subterms prove termination of tree recursion; lexicographic tuples handle nested phases; proper-subset orders can handle a shrinking finite work set. In each case the real obligation is the same:

$$I \land B \land V=v \quad\Longrightarrow\quad \text{after the body, } V \prec v,$$

where $\prec$ is well-founded. Current verifiers such as Dafny encode this as a decreases clause and check both loops and recursive calls against the same idea.

How to discover the invariant #

There is no complete mechanical recipe, but several moves are reliable.

1. Write the postcondition first. Replace the final index or collection with the loop's moving boundary. Lower bound's final partition becomes a partial partition around [lo, hi).
2. Record what has already been decided. A scan classifies a prefix; a two-ended algorithm classifies a prefix and suffix; a graph search separates discovered, finished, and undiscovered vertices.
3. Add safety bounds. State the relations that justify every index, dereference, division, and shift. Functional facts alone may not prove the body is defined.
4. Preserve input facts explicitly. Sortedness, an original multiset, or a root pointer may be needed later. Ghost variables can name initial values without changing runtime behavior.
5. State the frame. Say what the body may modify. Otherwise a heap-aware proof must conservatively forget unrelated facts after a call or mutation.
6. Test each obligation separately. Do not keep strengthening one assertion blindly; use the failed obligation to locate the missing fact.

Dijkstra's predicate-transformer view turns this around: start from the desired postcondition and calculate the weakest condition from which each statement guarantees it. For straight-line code this is systematic. Loops still require an invariant—the finite summary of an unbounded number of unfoldings—but backward calculation shows which facts the following code will demand.

Proof obligations are local, but assumptions are global #

A verifier typically translates a program and its annotations into verification conditions: logical formulas for initialization, preservation, postconditions, termination, framing, and run-time safety. An automated solver may discharge those formulas, but automation does not remove the trust boundary.

Check the complete envelope:

• Specification: does the contract express the actual requirement, including duplicates, empty inputs, exceptional outcomes, and permitted nondeterminism?
• Semantics: are integers bounded or mathematical, and what do overflow, division, shifts, floating-point values, and undefined behavior mean?
• State: can aliases, callbacks, threads, devices, or other processes mutate what the proof assumes stable?
• Control flow: do early returns, exceptions, cancellation, and retries pass through the invariant and postcondition boundaries?
• Resources: is “terminates” enough, or must memory, stack depth, I/O, and time also be bounded?
• Trusted base: which compiler, runtime, axioms, solver, foreign functions, and handwritten assumptions lie outside the proof?

Proof, tests, and runtime checks answer different questions #

A proof establishes a universal claim over its model. A test executes finitely many concrete cases against an implementation. A runtime assertion observes one execution. None subsumes the others.

• Proof is strongest for quantified boundaries and state-space coverage, but can faithfully prove a mistaken contract.
• Testing checks the executable artifact, integration, and assumptions that were omitted from a model; it can find counterexamples but cannot establish a universal claim from samples alone.
• Runtime assertions detect assumption violations in deployed executions, but only on reached paths and only when enabled.

Use the same invariants across all three layers when practical: as proof annotations, as property-based test oracles, and as carefully placed internal assertions. The invariant then becomes an executable statement of the algorithm's design rather than a proof artifact written after the fact.

A compact correctness workflow #

1. State the input domain, precondition, postcondition, exceptional behavior, and mutation frame.
2. Choose the exact data representation and language semantics.
3. For every loop, write initialization, preservation, exit, safety, and decrease obligations.
4. For every recursive routine, write a smaller-call relation and prove it is well-founded.
5. Derive the code and assertions together; a stubborn obligation is evidence about either one.
6. Inspect vacuous contracts and unproved assumptions before celebrating a green verifier.
7. Test the executable boundary and adversarial edge cases that connect the mathematical model to the real runtime.

The central habit is simple: never say “the algorithm obviously works.” Name the states it accepts, the fact each step preserves, the measure by which it progresses, and the exact result forced when no work remains.