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 welldescribed. 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.
Section 6.1, “The sequence rule”: do A
, then do B
.
Section 6.2, “The alternation rule”: if condition
A
is true, then do B
, otherwise do C
.
Section 6.3, “The definite iteration rule”: for every member
of some sequence S
, do
A
.
Section 6.4, “The while
loop rule”: while condition A
is true, do B
.
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 functionC
, must have the same net effect as doing the intended function forA
.
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*(n1)) ] variance = (sumData**2  sumSq)/(n*(n1)) # 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 
Σ data _{i}

sumSq 
Σ data _{i}^{2}

n  len(data) 
After prime 2, to find the value of variance
,
we substitute the expressions for sumData
and
sumSq
into the expression on the righthand
side to get this value:
variance 
[(Σ data _{i})  (Σ data _{i}^{2})] /
[len(data) *
(len(data)1 )]

After prime 3, we substitute that value of variance
into the righthand side to get the final
value:
result 
sqrt{[(Σ data _{i})  (Σ data _{i}^{2})] /
[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.