Submitted by egdaylight on
Dated:
In his 1972 `Notes on Structured Programming' [1, Chapter 1], Dijkstra introduced a methodology called step-wise program composition. He explained how to compose a program in minute steps, deciding each time as little as possible so that the correctness of each step is obvious.
Dijkstra applied his step-wise program composition on multiple problems in his `Notes on Structured Programming'. One problem was to instruct a computer to print a table of the first 1000 prime numbers. Dijkstra's step-wise composition of this problem into imperative code has also been investigated by Maarten van Emden on his blog. Another problem was, roughly stated, to let a computer print an image on paper.
Each step in Dijkstra's step-wise composition corresponds to a decision choice. General decision choices are made first, followed by more problem specific choices.
[W]ith progressing refinement, more detail about the actual problem statement has been brought into the picture. [...] As a result, our first levels of refinement are equally applicable for the members of a whole class of problem statements. [1,p.41]
For the problem of computing prime numbers, Dijkstra only used nontrivial arithmetical facts about prime numbers at a relatively late stage in his step-wise composition. Likewise, for his printing problem where an image is made up of lines, Dijkstra first solely reasoned about the image as a holistic entity. Only at a later stage did he “explain away” the image in terms of lines. He subsequently only reasoned in terms of lines, irrespective of whether the lines constituted an image or not.
Zooming in on Dijkstra's prime-number example, here are the first three successive — and increasingly detailed — descriptions which lead towards an imperative program that is executable on a computer.
Description 0:
begin “print first thousand prime numbers” end
Description 1:
begin variable “table p”;
“fill table p with first thousand prime numbers”;
“print table p” end
Description 2:
begin “integer array p[1:1000]”;
“make for k from 1 through 1000 p[k] equal to the kth prime number”
“print p[k] for k from 1 through 1000” end
The previous descriptions help to clarify some of Dijkstra's terminology. Each line in Description 2 is, in this particular example, a refinement of the corresponding line in Description 1. Description 2 thus contains three refinements: the first one describes a resource, while the other two describe actions. Line 1 in Description 2 declares the resource array as a refinement of the abstract resource “table p” in Description 1. Likewise, Line 2 in Description 2 is a refinement of the more abstract action “fill table p with first thousand prime numbers” in Description 1.
Dijkstra subsequently refined both actions in Description 2 independently of each other (leading to Description 3, not shown above). The reason why Dijkstra was able to refine both actions independently was because of his insistence to generalize as much as possible: the printing action is applicable in several contexts, not solely in the specific context of printing prime numbers.
Generalization thus prevailed, once again, in Dijkstra's thinking. This led him to consider a whole program family. Description 0, for instance, captures a family of programs, each of which prints the same numbers onto some medium. In Dijkstra's words:
[I]t is a very worth-while exercise to look for feasible generalisations of conceivable utility, because such considerations may give clear guidance as to how the final program should be structured. But such considerations boil down to ... conceiving (more or less explicitly) a whole program family! [1,p.41]
[1] O.-J. Dahl, E.W. Dijkstra, and C.A.R. Hoare. Structured Programming. Academic Press, London - New York - San Francisco, 1972.