EWD316: A Short Introduction to the Art of Programming
by
prof.dr.Edsger W.Dijkstra
August 1971
0. Contents
1. Preface
2. Some Fundamental Notions
3. Programming Languages and their Implementation
4. Variables and relations between their values
5. Programs corresponding to recurrence relations
6. A first example of step-wise program composition
7. The shortest spanning subtree of a graph
8. The towers of Hanoi
9. The problem of eight queens
10. A rearranging routine
4. Variables and relations between their values
When introducing the basic notions we have said that different happenings could take place following the same pattern of behaviour. And as the happening is fully determined by the confrontation of the pattern of behaviour with the initial state, it follows that the same pattern of behaviour can only evoke different happenings on different occasions when at these different occasions the initial states differ from each other. In this section we shall show how so-called variables are used for the description of the initial (and final) states. We find the typical use of variables when the same pattern of behaviour is followed repeatedly, i.e. when sequencing is repetitively controlled.
We begin with a very simple program: given two positive integer values A and B, a program has to be made that will compute (i.e. can cause a computer to compute) the Greatest Common Divisor of A and B. Let us use the notation GCD(A, B) for that value.
(Remark. We have restricted ourselves to positive numbers in order to make life somewhat easier. Zero is divisible by any positive integer D (for 0 = D * 0), and there would be no objection with B > 0, to
GCD(0, B) = B .
But admitting zero as argument is asking for trouble, because GCD(0, 0) is clearly undefined! In order to avoid these complications, we restrict ourselves to positive arguments.)
For the sake of argument we request an algorithm in which no arithmetic operators other than addition and subtraction will be used. How do we find such an algorithm?
Well, there seem in this case to be two ways of attacking the problem. The first one is more or less a direct application of the definition. One could construct a table of divisors of A (including 1) and a table of divisors of B (also including 1); as both A and B are finite and different from zero, both tables contain only a finite number of numbers. From these two tables of divisors one can construct a third table of common divisors, i.e. containing all the numbers in both of them. This third table is non-empty (because it contains the number 1) and it is finite (because it cannot be longer than any of the original tables). From this non-empty, finite table we can select the greatest number and that will, by virtue of the way in which it has been found, be the Greatest Common Divisor.
We could do it along the lines just sketched (or at least use it as a source of inspiration). In the current example, however, there is a second line of attack because the GCD is a well-known mathematical function, "well-known" meaning that a number of its properties are known. If we can think of so many of its properties that they define the GCD —i.e. that the GCD is the only function satisfying them— we might try to determine GCD(A, B) by exploiting these properties. What properties can we think of?
1) GCD(a, b) = GCD(b, a)
2) GCD(a, b) = GCD(a + b, b) = GCD(a, a + b)
3.1) if a > b: GCD(a, b) = GCD(a - b, b) = GCD(a, a - b)
3.2) if a = b: GCD(a, b) = a = b
3.3) if a < b: GCD(a, b) = GCD(a, b - a) = GCD(b - a, b)
(We can think of other properties, such as
4) for n ≥ 0: GCD(a^{n}, b^{n}) = GCD(a, b)^{n}
5) for c > 0: GCD(c * a, c * b) = c * GCD(a, b) ,
but they look less promising as they involve multiplication and we have to restrict ourselves to the arithmetic operations of addition and subtraction.)
The first property states that the GCD is a symmetric function. The second one states that the GCD of two numbers is equal to the GCD of one of them and the sum, while the third property states this for the difference. Because we want to restrict ourselves to positive numbers, we have dealt with the cases a < b and a > b separately. The case a = b, however, is very special: it is the only case in which the value of the GCD is given directly.
Relations 2, 3.1 and 3.3 tell us that the GCD of a pair of numbers is equal to the GCD of another pair of numbers. This suggests that we use the "current state" to fix such a number pair; the algorithm can then try to change these numbers in such a way that
firstly: | the GCD remains constant |
secondly: | until eventually the two numbers are equal and rule 3.2 can be applied. |
With the second requirement in mind, rule 2 does not look too promising: given two positive numbers, one of them never can be equal to their sum. On the other hand, given two (different!) positive numbers, one of them, viz. the smallest, can be equal to their difference. This suggest that from 3.1 and 3.3 we use:
3.1' if a > b: GCD(a, b) = GCD(a - b, b)
3.3' if a < b: GCD(a, b) = GCD(a, b - a) .
Now the moment has come to consider the first version of the program:
program1:
begin integer a, b, gcd;
a:= A; b:= B;
while a ≠ b do
if a > b then a:= a – b
else b:= b – a
gcd:= a;
print(A); print(B); print(gcd)
end
(In this program we have used the well-known alternative connective "if … then … else". The construction
"if inspection then action1 else action2"
causes one of two actions, either action1 or action2 to take place. If the inspection delivers the value true, action1 will take place (and action2 will be skipped); if the inspection delivers the value false, (action1 will be skipped and) action2 will take place. We can describe the conditional connective in terms of it:
"if inspection do action"
is equivalent to
"if inspection then action else nothing" ) .
When we try to understand this program we should bear the following in mind:
While the typical use of variables manifests itself with the program loop, the way to understand such a program implies looking for the relations between their values which remain invariant during the repetition.
In this example the invariant relation P is
P : a > 0 and b > 0 and GCD(a, b) = GCD(A, B ) .
The relation P holds after initialization (for then a = A and b = B ; from A > 0 and B > 0, relation P then follows).
The repeatable statement will only be executed under the additional condition a ≠ b; i.e. either a < b or a > b. If a > b, then the new value of a, viz. a – b, will again be positive and GCD(a, b) will remain unchanged on account of 3.1'; if a < b, the new value of b will again be positive and GCD(a, b) will remain unchanged on account of 3.3'. The invariance of relation P is therefore established.
When the loop terminates, a = b is guaranteed to hold, GCD(A, B) = GCD(a, b) = GCD(a, a) and on account of 3.2 the assignment "gcd := a" will establish the net effect "gcd := GCD(A, B)".
To complete the proof we must demonstrate that the repetition will indeed terminate. Whenever the repeatable statement is executed, the largest of the two (different!) values is decreased by the value of the other which is positive; as a result
max(a, b)_{T0} > max(a, b)_{T1}
We also know that before the repetition max(a, b) = max(A, B) is finite; from the invariance of the relation P (a > 0 and b > 0) we conclude that
max(a, b) > 0
will continue to hold. All values being integer, the maximum number of times the repeatable statement can be executed must be less than the max(A, B) and therefore the repetition must terminate after a finite number of repetitions. And this completes the proof.
Once we have this program, it is not difficult to think of others. Reading program1 we observe that each subtraction is preceded in time by two tests, first a ≠ b and then a > b; this seems somewhat wasteful as the truth of a > b already implies the truth of of a ≠ b. What happens in time is that a number of times a will be decreased by b, then b will be decreased by a, and so on. A program in which (in general) the number of tests will be smaller is
program 2:
begin integer a, b, gcd;
a := A; b := B;
while a ≠ b do
begin while a > b do a := a – b;
while b > a do b := b – a
end;
gcd := a;
print(A ), print(B ), print(gcd)
end .
Exercise. Prove the correctness of program 2.
Exercise. Rewrite program 2 in such a way that the outer repeatable statement contains only one loop instead of two. Prove its correctness.
Before going on, it is desirable to give a more formal description of the kind of theorems that we use. (In the following I shall make use of a formalism introduced by C.A.R. Hoare.)
Let P, P1, P2, … stand for predicates stating a relation between values of variables. Let S, S1, S2, … stand for pieces of program text, in general affecting values of variables, i.e. changing the current state. Let B, B1, B2, … stand for either predicates stating a relation between values of variables or for pieces of program text evaluating such a predicate, i.e. delivering one of the values true or false without further affecting values of variables, i.e. without changing the current state.
Then P1 { S } P2
means: "The truth of P1 immediately prior to the execution of S implies the truth of P2 immediately after that execution of S ". In terms of this formalism we write down the following theorems. (Some readers would prefer to call some of them rather "axioms" or "postulates", but at present I don't particularly care about the difference.)
Theorem 1:
Given: | P1 { S1 } P2 |
P2 { S2 } P3 | |
Conclusion: | P1 { S1; S2 } P3 |
(This theorem gives the semantic consequences of the semicolon as connective.)
Theorem 2:
Given: | B { S } non B |
Conclusion: | true { if B do S } non B |
(Here "true" is the condition which is satisfied by definition, i.e. the conclusion that after the execution of the conditional statement "non B " will hold, is independent of any assumptions about the initial state.)
Theorem 3:
Given: | (P and B ) { S } P |
Conclusion: | P { if B do S } P |
Theorem 4:
Given: | (P1 and B ) { S1 } P2 |
(P1 and non B ) { S2 } P2 | |
Conclusion: | P1 { if B then S1 else S2 } P2 |
Theorem 5:
Given: | (P and B ) { S } P |
Conclusion: | P { while B do S } (P and non B ) |
Remark: This theorem only applies to the case that the repetition terminates, otherwise it is void.
Theorem 5 is one of the most useful theorems when dealing with loops. The appropriate reasoning mechanism to deal with loops is mathematical induction, but often the use of Theorem 5 (which itself can only be proved by mathematical induction) avoids a direct use of mathematical induction.
We used Theorem 5 when proving the correctness of program1. Here was
P: a > 0 and b > 0 and GCD(a, b) = GCD (A, B ) and
B: a ≠ b .
We draw attention to the fact that we could not show "P { S } P " but only "(P and B ) { S } P ": for a and b to remain positive it was necessary to know that initially they were different. (How is this with program2?) We also draw attention to the fact that after termination, when we wished to show that a = GCD(A, B ), we did not only use the mild conclusion "P " bur the strong conclusion "P and non B ": we need the knowledge that a = b in order to justify the application of 3.2.
With respect to termination one often uses a somewhat stronger theorem, the formulation of which falls outside the strict Hoare formalism:
Theorem 6:
Given: | (P and B ) { S } P |
Conclusion: | in P { while B do S } the relation (P and B ) will hold immediately after each execution of the repeatable statement that is not its last execution. |
This theorem often plays a role when deriving a contradiction from the assumption that the loop will not terminate.