What “correct” means

Before you can show that code is correct, you need to say exactly what it should do. That statement is called a specification, or spec. Without one, “correct” has no meaning.

A promise about inputs and outputs

A specification describes what a function must do, without saying how. It has two parts:

• the input condition: what must be true of the inputs before the call;
• the promise: what will be true of the answer, if the input condition was true.

Here is a spec for a function that finds the largest value in a list:

def largest(a):
    """Input condition: a is a list of numbers, and it is not empty.
    Promise: returns m, where m is in a,
             and no value in a is bigger than m."""

A function is correct if, for every input that meets the input condition, the promise holds. Not for most inputs. For every one.

Input conditions and promises

Each side has its own job. The caller must meet the input condition. The function must keep the promise. If the caller passes an empty list, the spec promises nothing, and the function may do anything: return a wrong value, or raise an error.

Notice that the promise has two parts, and both are needed. “No value in a is bigger than m” alone is true for m = 1,000,000. “m is in a” rules that out. A weak spec lets wrong code pass.

Step through the figure. It runs two versions of largest on five inputs and checks each part of the promise. One version starts with best = 0. Find the input that breaks it.

Edge cases

Most bugs show up at the edges of the input condition: the smallest inputs and the unusual ones. The version with best = 0 works on every list that holds a positive number. It fails only when every value is negative. A few random tests could easily miss that.

Before writing any code, list the edge cases the spec allows. For a list, ask:

• Can it be empty? Can it have just one value?
• Can values repeat? Can they be negative, or zero?
• Is the answer at the very start, or the very end?
• What happens with the largest input the limits allow?

The test rows in every practice problem start with exactly these cases. Each one exists because students got it wrong.

The right answer, and it stops

Showing that a function is correct has two parts:

1. If it returns, the answer keeps the promise. This is called partial correctness.
2. It always returns. It never runs forever. This is called termination.

You need both. A loop that never ends never returns a wrong answer, so it is partially correct, but it is still useless. The next lesson shows how to prove each part for a loop.