IMPORTANT NOTE: This has been moved to here. The notes below are not up to date, and will soon be deleted.

Invariants

A programing invariant is a fact that is true at a particular point in a program. For example, consider this function:

// returns 1 + 2 + ... + n; n must be greater than 0
int sum_to(int n) {
    // Invariant: n > 0
    int result = 0;
    for(int i = 1; i <= n; i++) {
        // Invariant: 1 <= i <= n
        result += i;
    }
    // Invariant: result == (1 + 2 + 3 + ... + n)
    return result;
}

Three invariants are listed:

• The first invariant is a pre-condition, and asserts that n is greater than 0, i.e. that n > 0 is true.
• The second invariant is a loop invariant, and asserts that at the start of each iteration of the for-loop, i is between 1 and n.
• The third invariant is a post-condition, and asserts that, after the loop is done, result is equal to the sum of the numbers from 1 to n.

Checking Invariants with assert

A convenient way to automatically check some assertions is to use the assert macro. For example:

// returns 1 + 2 + ... + n; n must be greater than 0
int sum_to(int n) {
    assert(n > 0);
    int result = 0;
    for(int i = 1; i <= n; i++) {
        assert(1 <= i && i <= n);
        result += i;
    }
    // Invariant: result == (1 + 2 + 3 + ... + n)
    return result;
}

The first two invariant comments have been replaced by calls to the assert macro. To use assert, pass it a boolean expression, i.e. and expression that evaluates to true or false. If the expression is true, then assert does nothing and the program runs as normal. But if the expression is false, then assert will immediately crash the program with an error message saying on which line number the assertion failed. This is useful for debugging.

Note that assert(false) will always crash if it is run, while assert(true) will never crash if it runs. An assertion like assert(n > 0) may, or may not, crash, depending upon the value of n.

What is a macro?

assert is a macro, and not a function. In C, macro are handled by the pre-processor, and they work somewhat like functions, except macros don’t evaluate their arguments. Functions always evaluate their arguments, e.g. the function call f(1+2) is the same as f(3) when f is a function. In contrast, if f were a macro, then f(1+2) and f(3) could return different results.

assert is a macro because that lets it access the line number on which the assert occurs in the source code, so that it can print that information when it fails. A regular function cannot access the line number it’s on. While C macros do have their uses, they are generally much harder to use than functions, and not often needed. So in this course we won’t discuss them beyond this use of assert.

Pre-Conditions and Post-conditions

Some of the most useful assertions are function pre-conditions and post-conditions. A function pre-condition asserts what must be true before a function is called, and a function post-condition asserts what will be true after the function finishes (assuming the pre-condition was true). Also, we assume that the post-condition mentions all changes, so that values not mentioned in the post-condition are assumed to be unchanged.

Together, a functions pre and post conditions form a specification, i.e. they say what a function should do.

Pre-conditions and post-conditions are typically written as comments before the function, e.g.:

// Pre-condition:
//    n > 0
// Post-condition:
//    returns 1 + 2 + ... + n
int sum_to(int n) {
    assert(n > 0);
    int result = 0;
    for(int i = 1; i <= n; i++) {
        assert(1 <= i && i <= n);
        result += i;
    }
    // Invariant: result == (1 + 2 + 3 + ... + n)
    return result;
}

It can be useful to think of pre and post conditions as forming a contract between the function and the code that calls it.

For sum_to to work properly, it requires that n > 0 be true. If it’s not, then sum_to cannot promise to work correctly. The post-condition is what sum_to promises will be true when its done, assuming the pre-condition was true when it was called. The code that calls sum_to is responsible for ensuring the pre-condition holds, while sum_to is responsible for ensuring the post-condition holds.

Notice that there’s no easy way to use assert to check the post-condition. sum_to is calculating that post-condition. This is typical: it is often easier to automatically check pre-conditions than post-conditions.

In practice, clear and precise pre and post conditions is a valuable programming technique. The more important or complex a function, the more precise you should make the pre and post conditions.

Loop Invariants

A loop invariant is an invariant that occurs at the top of a loop body, e.g.:

int result = 0;
for(int i = 1; i <= n; i++) {
    assert(1 <= i && i <= n);  // loop invariant
    result += i;
}

Loop invariants are often quite helpful. Even if you don’t use assert they can help you think about loops.

Some loop invariants are more helpful than others. For example, here’s a useless loop invariant:

int result = 0;
for(int i = 1; i <= n; i++) {
    assert(2 == 2);  // loop invariant
    result += i;
}

2 == 2 is always true, so asserting here doesn’t help.

A slightly more useful loop invariant is this:

int result = 0;
for(int i = 1; i <= n; i++) {
    assert(i-1 <= result);  // loop invariant
    result += i;
}

From examining the loop we can see that the result is indeed always greater than, or equal to, i - 1. That’s because result starts at 0 and only goes up in positive increments of i.

Notice that assert(i <= result) is not a loop invariant. The first time through the loop i is 1 and result is 0, and so i <= result is false.

This is also a loop invariant, but it is not as useful as the previous one:

int result = 0;
for(int i = 1; i <= n; i++) {
    assert(i-1 <= result + 500);  // loop invariant
    result += i;
}

The invariant i-1 <= result + 500 is implied by i-1 <= result, and so, while it is true, it’s not as useful. In practice it can be tricky to come up with useful loop invariants.

Questions

1. What is a programming invariant?
2. Explain how C’s assert macro works. Why is it a macro, and not a regular C function?
3. Explain what pre-conditions and post-conditions describe for a function.
4. What is a loop invariant? Where does it occur in a loop?