Testing the promise

Convert 3,600 seconds into hours, minutes and seconds, then convert the result back, and you recover the original 3,600. That check passes, and it keeps passing for a program that returns an hour of zero, a minute of zero and a seconds field of 3,600, which no clock face can possibly display. A test is one clause of a promise executed on particular values, and the check above tests exactly one clause. The program that slips through nonetheless satisfies that clause completely.

So the question in this section's title has a sharper answer than it first appears. You do not learn that a program kept its contract by testing it; you learn that it kept one clause of that contract, on the values you chose to try, and only on those values. What a contract contains has already been settled: four lines, namely what you may pass in, what comes back, what stays the same, and what is not promised. The first three lines can be sampled on finitely many calls, and the first of them by choosing data that satisfies it. The fourth cannot be sampled at all, for a reason that occupies the remainder of this section. !Tests are finitely many points inside the precondition. The rectangle is every case the caller might ask about; the shaded region is the precondition, and the dots are the calls a test suite tries. The first three contract lines are sampled at those dots. The fourth line is a claim about the cases no dot reaches, including the calls nobody makes, so no number of dots can establish it. Status: schematic.

Four failures can meet the scorer, and each belongs to one line of the contract. Supply an empty table and the first check objects: with no rows the average divides zero by zero, and the caller broke a rule about what may be passed in. Alter a single charge and the number that comes back is wrong while nothing else complains: the procedure broke a rule. Let the scorer sort the table and the table comes back changed, while the first two checks stay silent. Run a procedure that loops forever and nothing comes back at all.

The first rule is the caller's obligation, and it has a name: a precondition states what every caller must establish before the call. The second is the procedure's obligation: a postcondition states what is true of the returned value. The third is the frame, the list of things that must come back unchanged. The fourth failure leaves no output to make a promise about, so the second line holds only if the procedure terminates [S:5:147]. Partial correctness is the property that the final results, if any, satisfy what was required of them; termination is the property that a final value is produced at all [S:5:147].

Worked example. Write the three tests that check the first three lines of the scorer's contract, and then look at what is left.

Each test checks one line on chosen values. The precondition is checked on the table before the call: at least one row is present, and every row supplies both an elapsed time and a recorded answer, so the check inspects the data rather than the procedure. The postcondition is tested against numbers computed by hand: the scorer returns 4/12, which is 1/3, when the candidate is round down, and 3/12, which is 1/4, when the candidate is round to nearest. The third line is tested by copying the table before the call and comparing it afterwards, which catches a scorer that sorts or consumes its input.

Three checks are worth writing instead of one because each can fail while the others stay silent. A single number returned by a single call tells you nothing about which line broke.

The fourth line has no such test, and the reason is not that nobody has written one. A test runs the procedure on values you supply, and the fourth line is a claim about values the procedure is never run on. For the scorer it reads: nothing whatever is promised about a task that is not among the rows, whether that task is a thirteenth one or a thousandth. What establishes that sentence is an argument rather than a run, and the argument is one line long. The average is a sum over the rows you hold, a thirteenth task contributes no term to that sum, and so its value cannot move the number.

A third kind of check compares two procedures instead of comparing a value with a constant. Convert a count of seconds to a time, convert the time back, and require the original count; run that over many values, and you have checked a relation that no single call could express [S:14:180]. The relation deserves stating in full: for every whole number of seconds x, the round trip through hours, minutes and seconds must return x. Each procedure is correct on its own terms, and the combination is required to agree.

The limitation is arithmetic and it does not go away, however many values you add. Many values are not every value, and adding more values does not close the gap, since the next value is always untried, whatever the size of the set you have tried.

Two exits exist: generate the values mechanically so that many becomes a large and awkward number rather than a handful, or prove the claim so that every becomes attainable. The other cost is subtler. A test written against the wrong level of the program can fail while the code it examines is perfectly correct, because the check reached past an interface to a representation that was always free to change under it. A test is a promise about a promise, and it inherits every boundary that the code below it respects.

The formal statement. Write a correctness claim as a triple: a precondition, a statement, and a postcondition. Partial correctness is the property that when there is a result, it is correct; termination is the property that a result is produced [S:5:147]. The two together give total correctness. The second line of the contract is the postcondition read with the termination qualifier, while the contract as a whole is precondition, postcondition, frame and exclusion.

A test is a triple of its own: one argument, one run, one check. Passing at argument a establishes the postcondition at a and nothing else. A suite is a finite set of arguments, and it establishes the postcondition on that set. The contract is a claim about every argument satisfying the precondition, so a suite establishes the contract only when the suite exhausts the precondition.

The derivation. The scorer's fourth line takes one line to establish. Its value is the sum of the charges divided by the number of rows. A task that is not among the rows contributes no charge to the sum, so it cannot change the total, so it cannot change the score. That is a claim about all unseen tasks, and it is established by reading the definition rather than by running anything.

The lookup candidate of the previous section shows the other outcome. Its body answers zero for any elapsed time not among the twelve, so an unseen task does not leave the answer free; it fixes the answer at the default zero. Its fourth line is therefore empty, and the value it returns on a thirteenth task is fixed by a branch that the twelve rows never exercised.

An edge case. Take the round-trip check, which converts a count of seconds to a time and back and requires the original count [S:14:180]. A program that returns zero hours, zero minutes and a seconds field of 3,600 passes the check for 3,600 seconds, and no clock displays that time. The relation holds and the postcondition of the conversion, which should require the seconds field below sixty, fails.

The converse failure is worth stating too, because it makes the round trip look stronger than it is. A conversion to whole minutes loses the seconds, so the composition fails the round trip while each procedure keeps its own promise. A consistency check tests a relation between two procedures, and it is neither necessary nor sufficient for either one's postcondition.

What L1 hid, and why that was safe there. L1 said that the first three lines can be sampled on chosen calls. The refinement is that running checks finitely many points of those lines, and that coverage measures which statements ran rather than which claims hold [S:114:481]. A reader who has written a first test needs the distinction between testing some values and testing the contract. The worked example used three checks that fail in three different ways, so the reader saw the value of a suite before meeting its limit.

Where the analogy breaks. A test is a promise about a promise, and it transfers nothing to a caller. A caller who relies on a passing test relies on the developer's judgement, not on a guarantee, which is why the fourth line still has to be written by hand.

Where the idea comes from. The formal half starts with Floyd. His invariant principle says that a property true at the start of a process and preserved by every step holds at every reachable state [S:5:143]. Mathematics for Computer Science records that he formulated it in 1967, and that it is the induction principle in the clothing of state machines [S:5:144]. The same chapter separates partial correctness from termination, which is the distinction that makes the second line of a contract honest [S:5:147].

The aphorism that gives this section its edge is Dijkstra's: testing can show the presence of bugs but never their absence [S:14:109]. The constructive counterpart is the consistency check, a relation between two procedures required to hold over many values [S:14:180].

What the field has not settled. Which adequacy criterion for a test suite, if any, bounds the chance that a passing suite misses a violated postcondition. Coverage is the usual measure: the fraction of code a test activates [S:114:481]. Path coverage is at least as demanding as statement coverage, because a suite that covers every feasible path covers every statement that lies on a path. The standard example needs four tests for every path against two for every statement [S:114:482]. Neither count says anything about the postcondition, because a suite can cover every path of a body that was written to the wrong specification. The evidence that would settle the question for one domain is a corpus of programs with known postconditions and seeded defects. Detection rates reported against several coverage criteria would let the criterion and the miss rate be compared on the same tasks.

What depends on it. The most visible contemporary use of tests is as the definition of correctness for generated code. A benchmark of programming problems grades a sample by running unit tests and counting the problems solved, and the strongest selection rule there is the one that keeps a sample only if the tests pass [S:629:2]. That design inherits this section's limitation exactly: the tests are the specification, and a program that passes them has kept the clause they encode and no other.

What to read next. Read the state-machine section of Mathematics for Computer Science for the invariant principle and its use in proving termination [S:5:143]. Read the testing chapter of Introduction to Computer Science for unit, integration and system testing, and for the coverage ladder from statements to paths [S:114:481]. Read the debugging page of Think Python for the dictum as a teaching text quotes it, and note that the page names its author only as a legendary computer scientist [S:14:109]. The original statement is Dijkstra's "Notes on Structured Programming" (EWD249, 1970), in the section on the reliability of programs. Then write one property as a triple and try to establish it by argument rather than by running, which is the exercise this chapter leaves you.