Checking Invariants

In Chapter 1 we introduced the distinction between the static and dynamic views of a program. The compiler checks the static view: it reads your source code, analyses your types, and flags inconsistencies before the program runs. But a program that passes the type checker can still produce the wrong results. Types tell you what kind of value a function returns, but not whether that value is correct.

The properties a correct program must maintain beyond its types are called invariants. This chapter is about working with them: what an invariant is, how to identify the invariants in a problem, how to record them in a function's documentation so that others can find them, and how to test whether they hold.

This course focuses on unit tests, which test individual units of a program, usually single functions.

What Is an Invariant?

An invariant is a property that must hold for a value or a computation to be meaningful. In this course, invariants are usually properties that the type system cannot express or enforce.

We have already met an invariant. In the previous chapter, the Song type carried this comment:

typescript

type Song = {
  title: string;
  artist: string;
  durationSeconds: number; // must be positive
};

The comment records something the type cannot: number includes -30, but real songs cannot have negative durations. The invariant is that durationSeconds must be positive. The type checker accepts an object that violates this invariant:

typescript

// passes the type checker; violates the invariant
const broken: Song = {
  title: "Song A",
  artist: "Artist 1",
  durationSeconds: -30
};

This object has the right shape, so the static type check passes. But its meaning is wrong, because it violates the invariant. Any code that trusts the invariant can now behave incorrectly. Imagine a function summing the durations in a playlist: a negative duration would make the running total go down, when it should only ever grow. When an invariant fails, a value can no longer be trusted by the operations built on it, even though the code may type check.

Invariants are everywhere once you look for them: durations are positive, percentage scores sit between 0 and 100, counts are whole numbers. None of these facts appear in the types number, number, number. They are constraints that exist in the space between what the type allows and what the problem requires.

Identifying Invariants

At the function level, invariants attach in two places: to a function's inputs and to its output. For the rest of this chapter we will work with a single running example:

As the campus library, I want late fees computed from how many days late a book is returned, with a short grace period and a capped maximum, so that patrons are charged fairly and predictably.

Concretely, the library's late-fee policy is that a book returned up to 2 days late incurs no fee. After that grace period, the fee is $0.50 for each additional day, and the total fee never exceeds $10.

A function computing the fee will have this signature:

typescript

lateFee(daysLate: number): number

A precondition is an invariant that must be true of the arguments when the function is called. The parameter type admits any number: -4, 3.7, 40000. But daysLate is a count of days, so the function is only meaningful when daysLate is a whole number and at least 0. That restriction is the precondition on daysLate.

A postcondition is an invariant about what the function guarantees about its result, assuming the precondition held. The return type says only number, but the policy promises more: the fee is never negative, and it never exceeds $10. Each of those guarantees is a postcondition.

To identify these in your own functions, examine the gap between the type you have included in a signature and the type's meaning:

Identifying preconditions: For each parameter, ask: of all the values this type allows, which are meaningful? Any restriction you state is a precondition. Look for ranges, wholeness, non-empty strings, and relationships between parameters (for example, min <= max).
Identifying postconditions: For the result, ask: what can the caller rely on beyond the return type? Any guarantee you state is a postcondition.

A useful invariant statement has three qualities. It is precise: terms must be backed by definitions, and words like "valid" or "sensible" without qualification are not useful. It is testable: you can programmatically validate whether the invariant is true. And it is operational: it is strong enough that an implementation can rely on it.

For example, consider the invariant stated as: daysLate is reasonable. This is not precise, testable, or operational: it cannot be checked or relied upon.

In contrast, the invariant daysLate is a whole number and daysLate >= 0 can be turned directly into tests.

Documenting Invariants

The compiler checks types, but it does not know about the invariants that restrict the values in your code. A caller, a test author, or a future maintainer can only find these invariants if they are written down where the function lives, in its documentation.

We record invariants in the function's doc comment, alongside its purpose. Doc comments precede function declarations, and are formatted within /** <text comments> */. The comment also describes each parameter (@param) and the return value (@returns). For lateFee, the full documented function is:

typescript

/**
 * Computes the fee (in dollars) for a library book returned
 * daysLate days after its due date.
 *
 * The first 2 days are a grace period: no fee is charged.
 * After the grace period, the fee is $0.50 for each additional
 * day. The total fee never exceeds $10.
 *
 * Precondition: daysLate is a whole number and daysLate >= 0.
 *
 * @param {number} daysLate the number of days past the due date
 * @returns {number} the fee in dollars, between 0 and 10
 */
function lateFee(daysLate: number): number

Function Doc Comments

In TypeScript, // comments out the rest of a line. Anything between /* and */ is also a comment, and these comments can span multiple lines.

For function doc comments in this course, we'll use syntax that's consistent with JSDoc:

typescript

/**
 * Here you put a summary of the function foo
 *
 * Precondition: list any preconditions
 * Postcondition: list any postconditions
 *
 * @param {typeofParam1} param1Name a description of param1Name's purpose
 * @param {typeofParam2} param2Name a description of param2Name's purpose
 * @returns {typeofReturn} describe what the return value expresses
 */
function foo(param1Name: typeofParam1, param2Name: typeofParam2): typeofReturn

The Precondition: line restricts daysLate to the meaningful subset of number, and the clause "the total fee never exceeds $10" is a postcondition on the result.

Together, a function's documented preconditions and postconditions are often called its contract: the caller promises the preconditions, and the function promises the postconditions in return. Writing the contract down makes the invariants visible to others. The doc comment is where a test author will look to decide what to check, and as we will see below, every clause of a well-written contract becomes a test.

Invariants

You wrote invariants in CPSC 110 too, in your data definitions and signatures. A signature using Natural instead of Number was a precondition (whole and non-negative): the daysLate precondition above is exactly Natural. Likewise, an interval data definition like:

racket

; Fee is Number[0, 10]
; interp. a late fee in dollars

was an invariant statement: the type is Number, and the meaningful subset is 0 to 10. TypeScript's types are checked, but they cannot express intervals, so these statements move into the function's doc comment instead.

Testing Invariants

Tests are commonly kept separate from the code they validate. In all of the code we look at in this course, in line with common best practice, production code is stored in the src/ directory and all tests are stored in the test/ directory. The test/ directory can contain any number of test files, often in 1:1 correspondence with the files being tested in src/.

Each test file contains a number of test cases. As in Chapter 1, each test case has a name and a body. The name describes what the test is checking, and the body is a single assertion. The checkExpect calls we have been writing are assertions.

In the contract above, the late fee grace period is two days long. A test case that checks this, by ensuring that lateFee(2) returns 0, looks like:

typescript

test("no fee at the grace boundary", checkExpect(() => lateFee(2), 0));

Assertions are the core of any test case: they check that the code produces the expected output for a given input when it runs. The checkExpect assertion takes two arguments: a no-argument function wrapping the expression to evaluate, and the expected result. If the two values are equal, the test passes silently. If they differ, the framework reports what was expected and what was produced, pointing you to the failing test by name.

Each test case holds exactly one check. This keeps the name of the case an accurate description of the one behaviour it validates, and it means a failing suite tells you how many distinct expectations are broken rather than stopping at the first one inside a case.

Tests vs check-expect

ISL used check-expect as a standalone expression at the top level of a file. TypeScript's test wrapper is a small change in form. It names the check so the framework can report it. The idea is the same: write down what you expect and let the framework compare.

racket

(check-expect (late-fee 2) 0)

Running Tests

test and checkExpect are provided by the course toolkit, and each test file imports them at the top of the file with:

typescript

import {
    test,
    checkExpect
} from "@ubccpsc/210-toolkit/testing";

To run the tests, you can either open the testing feature within your IDE (we will demo this in class), or open the terminal view within your IDE (also an in-class demo) and execute pnpm test. The terminal is a text-based interface where you type commands for the computer to run and read their output.

When executed by either your IDE or your terminal command, the test framework executes every test case it can find in the test/ directory. Passing test cases are printed in green, and failing test cases are printed in red, along with what was expected and what was returned.

The Testing Process

So far we have treated tests as something you write for code that already exists. While you are learning, we strongly recommend writing the tests first. Writing tests first forces you to think about the expected behaviours of the code under test (the code your test case is validating) before you spend time implementing it.

A precise set of input/output pairs is very helpful when implementing the code. Before writing the implementation, run your tests to confirm they fail. Once the implementation is correct, the tests should pass. A test that passes before you have implemented the function tells you nothing.

For lateFee we are already in a position to do this. We have not written a line of the implementation, but the contract we documented above gives us everything we need: each clause from the function documentation becomes a test.

typescript

test("no fee on the day a book comes due",
    checkExpect(() => lateFee(0), 0)
);

test("no fee at the end of the grace period",
    checkExpect(() => lateFee(2), 0)
);

test("fee accrues on the first charged day",
    checkExpect(() => lateFee(3), 0.50)
);

test("fee accrues for each further day",
    checkExpect(() => lateFee(12), 5.00)
);

test("fee never exceeds the maximum",
    checkExpect(() => lateFee(30), 10.00)
);

The precondition also marks inputs that have no specified output. Since the precondition says daysLate >= 0, what happens if we pass -5 is unspecified: the caller has broken their half of the bargain, and the function promises nothing in return. We return to what a function should do about inputs like this at the end of this chapter.

To run these tests, lateFee must at least exist, or the compiler reports an error for every test that calls it. So we begin with a stub: a function with the right signature that returns a clearly wrong value.

typescript

function lateFee(daysLate: number): number {
    return -1;  // stub
}

We chose -1 deliberately. A fee is never negative, so every test is guaranteed to fail against the stub. (Had the stub returned 0, the grace-period tests would have passed before we wrote any real code.) Running the suite shows all five tests failing, which confirms that each of them can fail:

✗ no fee on the day a book comes due
      Expected: 0
      Received: -1
✗ no fee at the end of the grace period
      Expected: 0
      Received: -1
✗ fee accrues on the first charged day
      Expected: 0.5
      Received: -1
✗ fee accrues for each further day
      Expected: 5
      Received: -1
✗ fee never exceeds the maximum
      Expected: 10
      Received: -1

Now we implement the function. The preconditions and postconditions give us an idea of which conditions to put in our if statement.

typescript

function lateFee(daysLate: number): number {
    if (daysLate <= 2) {
        return 0;
    }
    return 0.5 * (daysLate - 2);
}

And if we run the tests again:

✓ no fee on the day a book comes due
✓ no fee at the end of the grace period
✓ fee accrues on the first charged day
✓ fee accrues for each further day
✗ fee never exceeds the maximum
      Expected: 10
      Received: 14

Four tests pass, but the last fails. The failure report tells us exactly where to look: lateFee(30) produced 14. Re-reading the specification reveals the problem: our implementation handles the grace period and the per-day charge, but we forgot the maximum entirely. The fix adds the missing behaviour:

typescript

function lateFee(daysLate: number): number {
    if (daysLate <= 2) {
        return 0;
    }
    const fee = 0.5 * (daysLate - 2);
    if (fee > 10) {
        return 10;
    }
    return fee;
}

All five tests now pass:

✓ no fee on the day a book comes due
✓ no fee at the end of the grace period
✓ fee accrues on the first charged day
✓ fee accrues for each further day
✓ fee never exceeds the maximum

The tests did not change. They were correct all along, because they were written from the specification, so they already checked the requirement our implementation forgot. If we had written our tests after the implementation, by reading our own code and checking that it does what it appears to do, we would probably not have thought to test the maximum: the first prototype of lateFee contained no hint that a maximum should exist. Tests written first follow the specification, while tests written afterwards tend to mirror the code, mistakes included.

Deriving Tests

We wrote the lateFee suite by instinct: read the specification, turn each clause into a test. That instinct served us well, but instinct alone does not tell you when a suite is complete enough. Two systematic techniques, equivalence class partitioning and boundary value analysis, turn that instinct into a method.

Equivalence Classes

The most direct way to choose test inputs is to divide the input space into equivalence classes: groups of inputs that the specification says should be handled the same way. You then choose at least one representative from each class.

The lateFee specification divides its input into three classes:

Class	Inputs	Behaviour
Grace period	0 to 2	Fee is 0
Accruing	3 to 21	Fee grows by $0.50 per day
Capped	22 and up	Fee is exactly $10

The table starts at 0, with no negative inputs anywhere, because of the precondition daysLate >= 0. The invariant we wrote in the doc comment defines the input space the suite must cover. Without it, we would not know whether lateFee(-5) was a missing class or a meaningless input.

The suite we wrote has a representative from each class: lateFee(0) and lateFee(2) for the grace period, lateFee(3) and lateFee(12) for accrual, and lateFee(30) for the cap. It caught our missing-maximum fault because it had a representative from the capped class, the class the implementation forgot.

Within a class, one representative is as informative as another. lateFee(12) and lateFee(15) both exercise the accruing class, so testing both adds almost no confidence beyond testing one. Counting tests is therefore a poor measure of a suite: a suite of lateFee(5), lateFee(8), and lateFee(15) has three checks but covers only one class, and would have passed our buggy, cap-free implementation without complaint.

Boundary Value Analysis

Equivalence class partitioning identifies the regions to test. Boundary value analysis identifies where within those regions to look most carefully: at the edges, where one class meets the next.

Bugs cluster at boundaries, because boundaries are implemented with comparisons, and comparisons are easy to get wrong by one. lateFee has two boundaries: between days 2 and 3 (grace ends, accrual begins) and between days 21 and 22 (accrual reaches the maximum). A boundary-focused suite checks the last input on each side:

typescript

test("last free day", checkExpect(() => lateFee(2), 0));
test("first charged day", checkExpect(() => lateFee(3), 0.50));
test("last accruing day", checkExpect(() => lateFee(21), 9.50));
test("first day at the maximum", checkExpect(() => lateFee(22), 10.00));

Consider a near-miss implementation in which the grace check was written daysLate <= 3 instead of daysLate <= 2.

typescript

// Near-miss implementation example
function lateFee(daysLate: number): number {
    if (daysLate <= 3) { // bug here
        return 0;
    }
    const fee = 0.5 * (daysLate - 2);
    if (fee > 10) {
        return 10;
    }
    return fee;
}

This fault is visible at exactly one input: lateFee(3) returns 0 instead of 0.50. Every other value in the entire domain, including a mid-class representative like lateFee(12), behaves correctly.

Our original suite does catch this fault, but only by luck: we happened to choose the boundary value 3 as a representative of the accruing class. Had we chosen 4 and 12 instead, every test we wrote would have passed.

Off-by-one faults are often invisible everywhere except at a single input value, so boundary value analysis puts those values in the suite by design rather than by chance.

The diagram below draws the whole input space as a line, with three equivalence classes separated by the two boundaries the suite must pin down.

svgbob Diagram — The three equivalence classes for daysLate.

Erroneous Outcomes

Every call to a function has one of two outcomes. A successful outcome is the one the function exists to produce. An erroneous outcome is any other result. Think about a bank account. A customer trying to withdraw more than their balance is not unusual, and the design must anticipate it. An erroneous outcome like this is not a bug. It is a foreseeable result that belongs in the function's contract, so the caller knows it can happen and what they will receive when it does. Because it is part of the contract, it is tested like every other clause.

To see both outcomes in one place, we extend the library example. The library allows each book loan to be renewed at most twice:

typescript

type Loan = {
  title: string;
  // invariant: a whole number, 0 <= renewalsRemaining <= 2
  renewalsRemaining: number;
};

Renewing a loan that still has renewals left is the successful outcome. Trying to renew a loan that has no renewals remaining is an erroneous outcome. It happens often, so the contract should say exactly what the caller gets back.

How do we encode an erroneous outcome? We could return null, but null says nothing about what went wrong, and it means different things in different languages. We could return a special value, say a Loan whose renewalsRemaining is -1. But a special value is easy to mistake for a real one: a caller who forgets to check for -1 carries on computing with a loan that does not exist, and nothing in the types warns them.

So that we can be clear about the outcome, and rely on the type checker to check that both outcomes are handled, we introduce a result type:

typescript

type Result<T, E> = { ok: true; value: T } | { ok: false; error: E };

Result is generic over two type parameters: T is the type of a successful value, and E is the type of the error. This is the same tagged-union idea from the previous chapter, with ok as the discriminator: a caller checks ok to learn whether it received a value or an error. A successful outcome is an ok: true result carrying the value, and an erroneous outcome is an ok: false result carrying an explanation. Because the function's return type is Result<Loan, string> rather than Loan, the compiler will not let a caller use the value without first checking ok, so the erroneous outcome cannot be overlooked by accident.

typescript

/**
 * Renews a loan, consuming one renewal.
 *
 * Precondition: loan satisfies the Loan invariant.
 * Postcondition: if any renewals remain, returns ok: true with a new
 * Loan with one fewer renewal remaining; otherwise returns ok: false
 * with an explanatory error.
 *
 * @param {Loan} loan the loan to renew
 * @returns {Result<Loan, string>} the renewed Loan on success, or an
 * error explaining why the loan could not be renewed
 */
function renew(loan: Loan): Result<Loan, string> {
    if (loan.renewalsRemaining === 0) {
        // running out of renewals is an erroneous outcome the contract anticipates
        return { ok: false, error: "No further loan renewals available" };
    }
    return {
        ok: true,
        value: {
            title: loan.title,
            renewalsRemaining: loan.renewalsRemaining - 1
        }
    };
}

The postcondition documents both outcomes and what the caller receives in each case, so both are tested the same way, with checkExpect, as we tested every clause of the lateFee contract:

typescript

const fresh: Loan = { title: "Clean Code", renewalsRemaining: 2 };
const exhausted: Loan = { title: "Clean Code", renewalsRemaining: 0 };

test("renewal succeeds while renewals remain",
    checkExpect(() => renew(fresh), {
        ok: true,
        value: { title: "Clean Code", renewalsRemaining: 1 }
    })
);

test("renewal is refused when no renewals remain",
    checkExpect(() => renew(exhausted), {
        ok: false,
        error: "No further loan renewals available"
    })
);

The values each check needs are named above the tests rather than inside them, because the body of a test case is a single check.

The second test confirms that a refused renewal produces the result the contract specifies. Testing an erroneous outcome is no different from testing a successful one: if the contract describes the outcome, check the outcome.

Precondition Violations

What about a call that breaks the precondition: renew on a Loan whose renewalsRemaining is -1, or lateFee(-5)? These are neither successful nor erroneous outcomes, because the contract says nothing about them. The caller has broken their half of the bargain, and the function promises nothing in return. Our lateFee returns 1.75 for lateFee(5.5), a number with no meaning under the policy, and this is not a defect in lateFee: 5.5 was never a permitted input. There is nothing to test, because there is no specified behaviour to test against.

So the choice between a precondition and an erroneous outcome is a design decision. A precondition keeps a function simple, and is appropriate when every caller is code you control and can trust to respect the restriction. An erroneous outcome costs a check and a Result, and is appropriate when callers cannot be trusted to respect the restriction. This is especially important when a value arrives from somewhere you cannot trust: a user, a file, a network, or another system. In that case the function checks the input and returns ok: false, so the caller receives a clear result instead of a meaningless one. Whichever you choose, write it down: a restriction that appears in neither the precondition nor the postcondition protects no one.

Triangulating Quality: Type Checking and Testing

The type checker and the test suite operate at different times. The type checker works statically on the source code, ruling out whole categories of invalid calls before the program runs. Tests work dynamically, checking specific behaviours by executing the function. They are complementary approaches: a program that passes every type check can still return the wrong value for a given input. And a program that passes all its tests may still fail on an input the test suite did not evaluate. Together they give confidence. Types narrow the space of programs that can even be written, and tests validate that the program you wrote does what you intended.

Documented invariants connect the two. The preconditions and postconditions in a function's doc comment record the part of the specification the compiler cannot see, and they are what the tests should check.

An invariant that is written down can be turned into a test suite, but one that lives only in someone's head cannot be checked by anything.

Checking Invariants ​

What Is an Invariant? ​

Identifying Invariants ​

Documenting Invariants ​

Testing Invariants ​

The Testing Process ​

Deriving Tests ​

Equivalence Classes ​

Boundary Value Analysis ​

Erroneous Outcomes ​

Precondition Violations ​

Triangulating Quality: Type Checking and Testing ​

Checking Invariants

What Is an Invariant?

Identifying Invariants

Documenting Invariants

Testing Invariants

The Testing Process

Deriving Tests

Equivalence Classes

Boundary Value Analysis

Erroneous Outcomes

Precondition Violations

Triangulating Quality: Type Checking and Testing