A recipe with a promise

Take the number two and ask for its square root by a method with four steps: guess a value, divide the number two by the estimate, average the two numbers, and repeat the operation. Starting from an initial guess of one, the successive estimates read 1, then 1.5, then 1.4167, then 1.4142 [S:13:57], and the decimal digits stabilise after three passes.

The sentence you would write on a blackboard, that the square root of two is the non-negative quantity whose square is two, is true of the answer and entirely useless for finding it. It tells you almost nothing about how to actually find the square root of a given number [S:13:56]. A program is the other kind of description, because it states what to do rather than what is true. Because somebody else will execute it, a program also states what you may rely on when you do. That second half is the promise, the statement of what a caller may rely on, which this section teaches you to write down. !A contract for the square-root routine, written on four lines. Line 1 names the input: a whole number whose root is wanted. Line 2 promises a number whose square is within 0.001 of that input; the struck-through wording beneath it, “the square root”, is the reading the line forbids. Line 3 says the input is unchanged. Line 4 names what is not promised: that the square of the estimate equals the input exactly. The strip runs the estimates 1.0000, 1.5000, 1.4167 and 1.4142, with the gap between square and input under each; gold marks 1.4142, the first estimate inside the tolerance. Status: schematic.

Say what is true of a thing and you possess declarative knowledge; say how to obtain one and you possess imperative knowledge [S:13:57]. The ordered sequence of operations inside a program constitutes imperative knowledge, and each named block of steps is a procedure carrying a promise about its behaviour to every individual who employs it. The promise itself has a technical name: a contract for a procedure states four things, namely what you may pass in, what comes back, what remains unchanged, and what is not promised.

Think of a vending machine. You insert a coin, press a button, and a named item drops into the tray. The printed card adjacent to the button is the contract: these coins, that item. What the card never states is that the item is beneficial for you.

The comparison breaks at the next step, because a machine can also malfunction. Termination is not a fifth line of the contract: it is the condition under which the second line is asserted, so a call that never returns keeps the contract and is still useless [S:5:147]. The final section of this chapter takes that condition up.

The square-root routine demonstrates why the second line has to state its tolerance. Its stopping rule is a tolerance: stop when the square of the estimate differs from your number by less than 0.001 [S:13:58]. That 0.001 bounds the square, not the answer, and the second line of the contract says so: "a number whose square is within 0.001 of the number you passed in", and not "the square root". For nine the distinction is small enough to miss, because an estimate slightly above three has a square within 0.001 of nine while the estimate itself is wrong only in the fourth decimal place.

A caller who reads 0.001 as a bound on the answer therefore believes the result exact to three places, and nothing in the first three lines corrects that reading. The fourth line is a separate matter, and the case that tests it is a call the contract means to exclude; a radicand below the tolerance is one, and the Deepen layer of this section takes it up.

Worked example. Here is a small table, constructed for this chapter and sufficiently small to check by hand. Twelve separate tasks were timed with a stopwatch, and somebody recorded the whole number of minutes for each one.

Two candidate rules claim to reproduce what the person wrote: round down divides the elapsed seconds by sixty and retains the whole part, while round to nearest divides and takes the closer whole number. Round down disagrees with the table on four rows, and round to nearest disagrees on three. Item twelve is an evident transcription slip: 240 seconds equals four minutes exactly, and the notebook records zero.

The contract for a procedure that scores one candidate rule against this table has four lines.

1. What you may pass in: a rule that returns a whole number of minutes for any whole number of seconds, together with a table of at least one row, each row containing an elapsed time and a recorded answer.
2. What comes back: one number, obtained by dividing the sum of the charges by the number of rows, where a charge is 0 on a row the rule gets right and 1 on a row it gets wrong.
3. What stays the same: the table is not modified.
4. What is not promised: nothing concerning a thirteenth task, and nothing concerning whether the recorded answers are correct.

The score for round down on these twelve rows is 4/12, which reduces to the fraction 1/3. Read that number as "wrong on four rows out of twelve", never as "wrong one time in three on subsequent tasks". The table promises to report what was written down; it does not promise that what was written down is correct, and it says nothing whatever about rows it does not contain.

The idea costs something, because a contract is only as reliable as its fourth line, and that line is a judgement about calls nobody has made yet. You cannot verify such a claim by executing the procedure, since the procedure is never evaluated on the inputs it excludes. This chapter supplies the necessary vocabulary for stating the line, and the subsequent chapter investigates what happens when the table you possess is not the world you will encounter.

The formal statement. Fix a procedure p. A contract for p consists of four parts. They are a precondition on the arguments, a postcondition relating the argument to the returned value, a frame naming the objects that must come back unchanged, and an exclusion clause naming the calls about which nothing is claimed. The procedure keeps the contract when, for every argument a satisfying the precondition, either the call never returns or it returns a value v satisfying the postcondition with every object in the frame unchanged.

That last sentence carries a qualifier the four-line form hides, because the second line holds only if the call finishes. Partial correctness is the property that a result, when produced, satisfies the requirement; termination is the property that a result is produced at all [S:5:147]. Read the second line as "if it returns, then this is true of what it returns".

The derivation. The square-root recipe iterates the map that averages the estimate with the number divided by the estimate, and stops when the square of the estimate differs from the number by less than the tolerance [S:13:58]. Write r for the exact non-negative root and y for an estimate that satisfies the stopping rule, and suppose the radicand is positive and the guess is non-negative. Then y^2 - r^2 = (y - r)(y + r), so the distance from the estimate to the root equals the error in the square divided by y + r. Because y is non-negative and r is positive, the denominator is at least r, and the distance to the root is at most the tolerance divided by r. The precondition of the procedure therefore names a positive radicand and a non-negative initial guess.

So the second line bounds the error in the square, and the error in the answer is that bound divided by the root. The two quantities coincide only when the root is near one.

The step I omit is the proof that the iteration enters the stopping region at all. That argument needs a contraction bound on the update map, and it belongs with the convergence material of Chapter 5 and the induction of Chapter 3.

An edge case. Take a positive number smaller than the tolerance. The estimate zero satisfies the stopping rule, because the square of zero differs from the number by less than the tolerance, and zero is wrong by the whole answer. The second line, read exactly as written, permits it. A contract that promises usable accuracy therefore has two options: state the tolerance relative to the root, or restrict the precondition to inputs above a floor.

What L1 hid, and why that was safe there. L1 described the promise as four lines and left the quantifier implicit. The refinement is that lines one to three are claims about every call satisfying the precondition, not about the calls you happen to make. For a reader meeting contracts for the first time, the universal quantifier adds nothing to the picture, and the worked example used a number whose root is close to one, where the absolute and relative readings nearly coincide.

Where the analogy breaks. The vending machine fails visibly: no item drops. A procedure can return a plausible value of the right type and the tray looks full. The machine's card never needs a fourth line because a malfunction announces itself, while a procedure that keeps the wrong promise is silent.

Where the idea comes from. The distinction that starts this section is in the opening of the square-root chapter of Structure and Interpretation of Computer Programs. The mathematical definition states what is true and the procedure states what to do [S:13:56]. The text names that pair declarative and imperative knowledge [S:13:57]. The four-line form is a synthesis rather than a quotation. Its first two lines are the precondition and postcondition of program correctness, and its third line is the frame condition of the same tradition. The invariant principle of Floyd gives the underlying method: a property true at the start and preserved by every step holds at every reachable state [S:5:143], and Floyd formulated it in 1967 [S:5:144].

The fourth line has a different ancestry. Testing practice separates specification-based testing, which works from requirements and needs no sight of the code, from structural testing, which works from the code [S:114:480]. A contract written on four lines is exactly what the first of those needs, because it is the whole of what a tester may assume.

What the field has not settled. Nobody has a cheap way to check the exclusion clause. A frame condition can be tested by copying an object and comparing it afterwards. An exclusion clause is a claim about calls that never happen, and the usual tools reach it only by proving something about the body. The open question is whether a specification language can be written whose checker rejects a wrong implementation while accepting a correct one, without the author paying for a full proof. The evidence that would settle it is a small suite of interchangeable implementations of one interface, with a checker that separates them by their declared exclusions alone.

What depends on it. Black-box testing depends on the idea directly: a test written against requirements rather than code is a test of the contract, and the vocabulary of preconditions and postconditions is what makes the test expressible [S:114:480]. The same vocabulary returns in Chapter 4, where a result is trusted only as far as the conditions of its run are recorded.

What to read next. Read SICP section 1.1.7 for the declarative and imperative split [S:13:56], then section 5.4 of Mathematics for Computer Science for the invariant principle and its use in proving programs correct [S:5:143]. Read the testing chapter of Introduction to Computer Science for the black-box and white-box distinction in practice [S:114:480]. Keep the page on partial correctness open beside them, because every promise in this book carries the same qualifier [S:5:147].