Next / Previous / Contents / Shipman's homepage

6. Proof rules and the stepwise refinement process


The required techniques of effective reasoning are pretty formal, but as long as programming is done by people that don't master them, the software crisis will remain with us and will be considered an incurable disease. And you know what incurable diseases do: they invite the quacks and charlatans in, who in this case take the form of Software Engineering gurus.

 -- Edsger J. Dijkstra, Answers to questions from students of Software Engineering

Once you have written the intended function for your entire script or other prime, use stepwise refinement to write the code.

If the implementation of the prime is trivial — a line or three of code — then you simply write the code. At that point you can proceed to apply the rules given in Section 7, “Standards for the review of intended functions”, construct trace tables (Section 8, “Trace tables”), and conduct peer reviews of the prime.

However, for any nontrivial application, you must figure out how to break the logic into smaller pieces. The basic idea of stepwise refinement is to divide each large piece into, say, two to seven smaller pieces, and continue subdividing until each piece is small and well-described. Every single interface between a larger piece and the smaller pieces that it uses must be completely defined. Our intended functions are the interface definitions that hold the entire design together.

Each time you subdivide your design into smaller pieces, you will also write the intended functions for each of the smaller pieces.

In order to be sure that we can reason mathematically about this process, the way you subdivide a prime into smaller pieces must fit one of these four standard patterns. For each pattern, there is a related proof rule that must be used during peer review to satisfy all present that the implementation is correct. Each proof rule describes how to compare the intended function for each of the smaller pieces of the prime against the overall intended function for the prime as a whole.

6.1. The sequence rule

When a prime A is subdivided into a sequence of two smaller primes B and C, the proof rule reads like this.

Doing the intended function for B, followed by doing the intended function C, must have the same net effect as doing the intended function for A.

Here is an example: the computation of the standard deviation of a tuple data containing float values. This is a sequence of three primes.

def stdDev(data):
    '''Return the standard deviation of a data set.

      [ data is an iterable containing at least two floats ->
          return the standard deviation of data ]
    #-- 1
    # [ sumData  :=  sum of data
    #   sumSq  :=  sum of squares of data
    #   n  :=  length of data ]
    sumData = sum(data)
    sumSq = sum([x**2
                 for x in data])
    n = len(data)

    #-- 2
    # [ variance  :=  ((square of sumData) - sumSq)/(n*(n-1)) ]
    variance = (sumData**2 - sumSq)/(n*(n-1))

    #-- 3
    # [ result  :=  square root of variance ]
    result = variance**0.5

    #-- 4
    return result

What value will this function return? To find out, we'll take it one prime at a time. After prime 1, these state items have changed:

sumData Σ datai
sumSq Σ datai2

After prime 2, to find the value of variance, we substitute the expressions for sumData and sumSq into the expression on the right-hand side to get this value:

variance [(Σ datai) - (Σ datai2)] / [len(data) * (len(data)-1)]

After prime 3, we substitute that value of variance into the right-hand side to get the final value:

result sqrt{[(Σ datai) - (Σ datai2)] / [len(data) * (len(data)-1)]}

The final prime returns this value. In order to convince ourselves that the returned value is correct, we can compare the value of result above with the formula for the standard deviation in a statistics reference.