A properly constructed intended function must describe exactly everything the code is to do, no more, and no less.

Additionally, there are a number of tests of correctness that you (as the author of the code) and reviewers must apply to your intended functions.

Every side effect of the code must be accounted for. If you change the value of a global variable, or send something over the Internet, you must declare it in your intended function.

There must be a balance between inputs and outputs between the intended function for a prime, and its breakout into smaller primes. In intended functions, any state item that appears on a right-hand side is an input, and any state item that appears on a left-hand side is an output.

This means that if a some state item is referenced in the right-hand side of the overall prime's intended function, there must be a reference to that state item in one of the pieces.

Conversely, if one of the pieces of a prime refers to some state item, then either that state item must be entirely local to the larger prime, or it must also be an input to the larger prime.

Also, a state item that appears on the left-hand side of the overall intended function must appear on the left-hand side of one of the pieces. That is, a net output of the overall prime must appear as an output of at least one its components.

All routes through the code must be covered; that is, consider all the possible cases.

If you don't want to deal with some case, you can formulate a precondition to make it the caller's responsibility to deal with that case.

For example, if you are writing a square root function, you have your choice of whose responsibility it is to deal with negative arguments. If you make it a precondition that the argument is nonnegative, it's the caller's fault if they pass you a negative argument.

def square_root(x): '''Compute the square root of x. [ x is a nonnegative number -> return the square root of x ] ''' ...

The other alternative is to state what your code will do in that case.

def square_root(x): '''Compute the square root of x. [ if x is a nonnegative number -> return the square root of x else -> raise ValueError ] ''' ...

We'll have more to say about case coverage in Section 8, “Trace tables”.