Assertions and Invariants

A specification written in a comment is a wish; a specification written as an assert is a wish the machine will check. An assertion is a boolean expression you plant in the code with the claim "at this point in every execution, this is true" — and if it is ever false, the program stops and tells you, at the scene of the crime, instead of limping on and corrupting something three function calls later. Assertions are how the pre/postconditions of the last page stop being paper contracts and become executable ones.

The most powerful assertion is not attached to a single line but to an entire object: an invariant — a property that holds every time you look. This page is about the two together: assertions as executable specifications, and the invariants (data, representation, class) that keep a data structure honest between operations.

Assertions as executable specifications

The precondition of a routine becomes an assertion at its entry; the postcondition becomes an assertion at its exit. An assertion that guards entry is defensive programming: rather than trust callers, the routine checks the caller's obligation itself and refuses to proceed on garbage. The governing philosophy is fail-fast — detect the violated assumption at the earliest possible instant, because the distance (in time and stack frames) between a corruption and its symptom is exactly the cost of debugging it.

function isqrt(n: number): number { console.assert(n >= 0, "precondition violated: n must be non-negative"); // precondition let r = 0; while ((r + 1) * (r + 1) <= n) r = r + 1; console.assert(r * r <= n && (r + 1) * (r + 1) > n, "postcondition violated"); // postcondition return r; }

A crucial distinction: an assertion is not error handling. Error handling copes with situations that can legitimately happen at runtime — a missing file, a malformed request — and the program must recover gracefully. An assertion documents something the programmer believes cannot happen if the code is correct; if it fires, the code has a bug, and the right response is to abort, not recover. Put the other way: never validate untrusted external input with an assertion (which may be compiled out), and never try/catch around a logic bug. Assertions police internal consistency; exceptions handle external reality.

Invariants: properties that hold every time you look

An invariant is an assertion attached to a scope larger than a single statement. Three flavours matter, from the concrete outward:

A data invariant constrains the values a piece of data may take: "this list is sorted", "this date's month is in 1–12". It is a predicate over the fields.
A representation invariant (rep invariant) is the data invariant of a class's internal representation — the relationship among private fields that must hold for the object to represent a valid abstract value. Example: in a fraction stored as (\mathit{num}, \mathit{den}), the rep invariant is \mathit{den} > 0 \wedge \gcd(|\mathit{num}|, \mathit{den}) = 1.
A class invariant is a rep invariant promoted to a promise about the object's whole lifetime: it holds after the constructor, and it is re-established by the end of every public method. It may be temporarily broken in the middle of a method — that is fine, as long as no other code can observe the object while it is broken.

The class invariant is the load-bearing idea. It lets you reason locally: to trust a method, you assume the invariant on entry (the object was left valid by whatever ran before) and you must re-establish it on exit. Every public method is thus a little Hoare triple whose pre- and postconditions both include the invariant. The invariant is the glue that makes an object more than a bag of fields.

Worked example: a bounded stack with its invariant

A fixed-capacity stack stores its elements in an array \mathit{data} and a count \mathit{size}. The class invariant is 0 \le \mathit{size} \le \mathit{capacity} — the count never goes negative and never exceeds the array. Watch how each public method assumes it on entry and re-establishes it on exit, with preconditions guarded by assertions.

class BoundedStack { private readonly data: number[]; private size = 0; // class invariant: 0 <= size <= capacity constructor(private readonly capacity: number) { console.assert(capacity >= 0, "capacity must be non-negative"); this.data = new Array(capacity); this.checkInvariant(); // invariant holds right after construction } private checkInvariant(): void { console.assert(this.size >= 0 && this.size <= this.capacity, "rep invariant broken"); } push(x: number): void { console.assert(this.size < this.capacity, "precondition: stack is full"); // caller's obligation this.data[this.size] = x; this.size = this.size + 1; // invariant momentarily re-derived here this.checkInvariant(); // re-established on exit } pop(): number { console.assert(this.size > 0, "precondition: stack is empty"); // caller's obligation this.size = this.size - 1; const x = this.data[this.size]; this.checkInvariant(); // re-established on exit return x; } isEmpty(): boolean { return this.size === 0; } isFull(): boolean { return this.size === this.capacity; } }

Two things to notice. First, the preconditions of push (not full) and pop (not empty) are the caller's obligation — the class offers isFull/ isEmpty so callers can discharge them. Second, checkInvariant() is called after every mutation, so the class invariant is machine-checked at every public boundary. Because data and size are private, no outside code can put the object into a state that violates the invariant — encapsulation is what makes an invariant enforceable. Expose the fields and the invariant becomes a wish again.

Where an invariant lives during a method

The trace below follows push on a stack with capacity 3 currently holding 2 elements. The invariant 0 \le \mathit{size} \le 3 is true at the boundaries and — importantly — is briefly re-established only at the end, after both the array write and the counter bump.

Step	\mathit{size}	Invariant 0 \le \mathit{size} \le 3
on entry to `push`	2	holds
precondition \mathit{size} < 3 checked	2	holds
`data[2] = x`	2	holds
`size = size + 1`	3	holds (3 \le 3)
on exit (`checkInvariant`)	3	holds

Had the precondition \mathit{size} < \mathit{capacity} been skipped, a push at \mathit{size} = 3 would write data[3] out of bounds and bump \mathit{size} to 4 — the invariant \mathit{size} \le 3 shattered, and the assertion catches it on the very next line rather than letting a corrupt object escape.

Everything here is an invariant over a scope in space — a data structure, an object. There is a second, equally important kind that is an invariant over a scope in time: a loop invariant, a property that holds at the top of a loop on every iteration. They are the same idea wearing different clothes — "a condition that is preserved by each step" — and both are proved the same way: true when you enter, preserved by each operation (a push, or one trip round the loop). A class invariant is preserved by each public method; a loop invariant is preserved by each iteration of the body. Master one and the other is a short step: it is invariants, all the way down.

In many languages assertions are disabled in production for speed: Java runs without -ea by default, C's assert vanishes under NDEBUG, and a stripped build may drop console.assert too. So the golden rule: an assertion's expression must have no side effects. The catastrophe is code like assert(stack.pop() === 5) — in a debug build it pops and checks; in a release build the whole line disappears, the pop never happens, and the program behaves differently depending on a compiler flag. That is one of the nastiest bugs there is, because it cannot be reproduced in the debugger where assertions are on. Assertions are for checking state, never for changing it. Two corollaries: never use an assertion to validate untrusted external input (it may be compiled away, leaving the input unchecked), and never rely on an assertion's side effect for correctness — if the work must happen, do it on a normal line.