NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR

The formal treatment of some small examples.

In this chapter I shall give the formal development of a series of small programs solving simple problems. This chapter should not be interpreted as my suggestion that these programs must or should be developed in such a way: such a suggestion would be somewhat ridiculous. I expect most of my readers to be familiar with most of the examples and, if not, they can probably write down a program, hardly aware of having to think about it.

The development, therefore, is given for quite other reasons. One reason is to make ourselves more familiar with the formalism as far as it has been developed up to now. A second reason is to convince ourselves that, in principle at least, the formalism is able to make explicit and quite rigourous what is often justified with a lot of hand-waving. A third reason is precisely that most of us are so familiar with them that we have forgotten how, a long time ago, we have convinced ourselves of their correctness: in this respect this chapter resembles the beginning lessons in plane geometry that are traditionally devoted to proving the obvious. Fourthly, we may occasionally get a little surprise and discover that a little familiar problem is not so familiar after all. Finally it may shed some light on the feasibility, the difficulties and the possibilities of automatic program composition or mechanical assistance in the programming process. This could be of importance even if we do not have the slightest interest in automatic program composition, for it may give us a better appreciation of the role that our inventive powers may or have to play. In my examples I shall state requirements of the form “for fixed x, y, ... ; this is an abreviation for “for any values X0 , y0, ... a post-condition of the form x = x0 and y = y0 and ... should give rise to a pre-condition implying x = x0 and y = y0 and ”. We shall guarantee this by treating such quantities as “temporary constants”, they will not occur to the left of an assigment statement.

First example. Establish for fixed x and y the relation R(m):

Note. If the function “max” had been an available primitive, we could have coded m:= max(x, y) because R(max(x, y)) = T (End of note.)

The program we have derived is not very impressive; on the other hand we observe that in the process of deriving the program from our postcondition next to nothing has been left to our invention.

Second example.

For a fixed value of n (n > 0) a function f(i) is given for 0 ≤ i < n . Establish the truth of R:

In order to verify whether this choice of P can be used, we must have an easy way of establishing it to start with. Well, because

Again my experience suggests to choose as monotonicly decreasing function t of the current state t = (n - j) , which, indeed, is such that P ⇒ (t ≥0) . In order to ensure this monotonic decrease of t I propose to subject j to an increase by 1 and we can develop

The second remark is that having developed a correct program does not mean that we are through with the problem. Programming is as much a mathematical discipline as an engineering discipline, correctness is as much our concern as, say, efficiency. Under the assumption that the computation of a value of the function f for a given argument is a relatively time-consuming operation, a good engineer should observe that in all probability this program will often ask for many re-computations of f(k) for the same value of k . If this is the case the trading of some storage space against some computation time is indicated. The effort to make our program more time-efficient, however, should never be an excuse to make a mess of it. (This is obvious, but I state it explicitly because so much messiness is so often defended by an appeal to efficiency considerations, while upon closer inspection the defense is always unvalid: it must be, for a mess is never defensible.) The orderly technique for trading storage space versus computation time is the introduction of one or more redundant variables, the value of which can be used because some relation is kept invariant. In this example the observation of the possibly frequent re-computation of f(k) for the same value of k suggests the introduction of a further variable, max say, and to extend the invariant relation with the further term

This program is probably much more efficient than our previous version. If it is, a good engineer does not stop here, because he will now observe that for the same value of j he might order a number of times the computation of f(j). It is suggested to introduce a further variable, h say (short For “help”) and to keep

A final remark is not so much concerned with our solution as with our considerations. We have had our mathematical concerns, we have had our engineering concerns and we have accomplished a certain amount of separation between them, now focussing our attention on this aspect and then on that aspect. While such a separation of concerns is absolutely essential when dealing with more complicated problems, I must stress that focussing one’s attention on one aspect does not mean completely ignoring the others. In the more mathematical part of the design activity we should not head for a mathematically correct program that is so badly engineered that it is beyond salvation. Similarly, while “trading” we should not introduce errors through sloppiness, we should do it careful and systematic; also, although the mathematical analysis as such has been completed, we should still understand enough about the problem to judge whether our considered changes are significant improvements.

Note. Prior to my getting used to these formal developments I would always have used “j < n” as the guard for this repetitive construct, a habit I still have to unlearn, for in a case like this, the guard “j ≠ n” is certainly to be preferred. The reason for the preference is twofold. The guard “j ≠ n” allows us to conclude j = n upon termination without an appeal to the invariant relation P and thus simplifies the argument about what the whole construct achieves for us compared with the guard “j < n”. Much more important, however, is that the guard “j ≠ n” makes termination dependent upon (part of) the invariant relation, viz. j ≤ n and is therefore to be preferred for reasons of robustness. If the addition j:= j + 1 would erroneously increase j too much and would establish j > n , then the guard “j < n” would give no alarm, while the guard “j ≠ n” would at least prevent proper termination. Even without taking machine malfunctioning into account, this argument seems valid. Let a sequence x0, x1, x2, ... be given by a value for x0 and for i > 0 by x_i= f(x_i-1) , where f is some computable function and let us carefully and correctly keep the relation X = x_i, invariant. Suppose that we have in a program a monotonicly increasing variable n , such that for some values of n we are interested in x_n . Provided n ≠ i , we can always establish X = x_n by

Third example.

For fixed a (a ≥ 0) and d (d > 0) it is requested to establish

For the function t , the decrease of which should ensure termination, we choose r itself; because the messaging of r must be such that the relation (a - r)|d is kept invariant, r may only be changed by a multiple of d , for instance d itself. Thus we find ourselves invited to evaluate

Because the term d > 0 could have been added to the invariant relation P , only the first term is then not implied; we find the corresponding guard “r ≥ d” and the tentative program:

Suppose now, that in addition it would have been required to assign to q such a value that finally we also have

We can speed up our first program by replacing “r:= r - d” by a possibly repeated decrease of r by dd , while dd , initially = d , is allowed to grow rather rapidly, e.g. by doubling it each time. So we are led to consider the following program

But the above reasoning —although convincing enough!— is a very informal one and because this chapter is called “a formal treatment” we can try to formulate and prove the theorem to which we have appealed intuitively.

With the usual meanings of IF, DO and BB , let P be the relation that is kept invariant, i.e.

Exercise. Modify also our second program in such a way that it computes the quotient as well and give a formal correctness proof for your program.

Let us assume next, that there is a small number, 3 say, by which we are allowed to multiply and to divide and that these operations are sufficiently fast so that they are attractive to use. We shall denote the product by “m * 3” —or by “3 * m”— and the quotient by “m / 3”; the latter expression will only be called for evalution provided initially m|3 holds. (We are working with integer numbers, aren’t we?)

Again we try to establish the desired relation R by means of a repetitive construct, for which the invariant relation P is derived by replacing a constant by a variable. Replacing the constant d by the variable dd , whose values will be restricted to d *(a power of 3) we come to the invariant relation P:

Exercise. Modify also the above program in such a way that it computes the quotient as well and give a formal correctness proof for your program. This proof has to demonstrate that whenever dd / 3 is computed, originally dd|3 holds. The above program exhibits a quite common characteristic. On the outer level we have two repetitive constructs in succession; when we have two or more repetitive constructs on the same level in succession, the guarded commands of the later ones lend to be more elaborate than those of the earlier ones. (This is known as “Dijkstra’s Law”, which does not always hold.) The reason for this tendency is clear: each repetitive construct adds his “and non BB” to the relation it keeps invariant and that additional relation has to be kept invariant by the next one as well. But for the inner loop, the second one is exactly the inverse of the first one; but it is precisely the function of the added statement do r ≥ dd → r:= r - dd od to restore the potentially destroyed relation r < dd , i.e. the achievement of the first loop.

Fourth example.

For fixed Q1 , Q2 , Q3 and Q4 it is requested to establish R where R is given as R1 and R2 with R1: The sequence of values (q1, q2, q3, q4) is a permutation of the sequence of values (Q1, Q2, Q3, Q4) R2:         q1 ≤ q2 ≤ q3 ≤ q4 .

Taking R1 as relation P to be kept invariant a possible solution is

Note. Observe that we could have added other alternatives such as

It is a nice example of the kind of clarity that our non-determinacy has made possible to achieve; needless to say, however, that I do not recommend to sort a large number of values in an analogous manner.

Fifth example.

We are requested to design a program approximating a square root, more precisely: for fixed n (n ≥ 0) the program should establish

One way of weakening this relation is dropping one of the terms of the conjunction, e.g. the last one and focus upon

This program is not very surprising, it is not very efficient either: for large values of n it could be rather time-consuming. Another way of generalizing R is the introduction of another variable, b say —and again restricting its range— that is to replace part of R, for instance

The use of the operator div suggests that we should look what happens if we impose upon ourselves the restricition that whenever d is computed, b - a should be even. Introducing c = b - e and eliminating the b , we get the invariant relation

Under admission of the danger of beating this little example to death, I would like to submit the last version to yet another transformation. We have written the program under the assumption that sqaring a number is among the repertoire of available operations, but suppose it is not and suppose that multiplying and dividing by (small) powers of 2 are the only (semi-)multiplicative operations at our disposal. Then our last program as it stands is no good i.e. it is no good if we assume that the values of the variables as directly manipulated by the machine are to be equated to the values of the variables a and c if this computation were performed “in abstracto”. To put it in another way: we can consider a and c as abstract variables whose values are represented —according to a convention more complicated than just identity— by the values of other variables that are in fact manipulated by the machine. Instead of directly manipulating a and c , we can let the machine manipulate p , q and r , such that

This fifth example has been included because it relates —in an embellished form— a true design history. When the youngest of our two dogs was only a few months old I walked with both of them one evening, preparing my lectures for the next morning, when I would have to address students with only a few weeks exposure to programming, and I wanted a simple problem such that I could “massage” the solutions. During that one hour walk the first, third and fourth program were developed in that order, but for the fact that the correct introduction of h in the last program was something I could only manage with the aid of pencil and paper after I had returned home. The second program, the one manipulating a and b , which here has been presented as a stepping stone to our third solution, was only discovered a few weeks later —be it in a less elegant form then presented here. A second reason for its inclusion is the relation between the third and the fourth program: with respect to the latter one the other one represents our first example of so-called representational abstraction.

Sixth example.

For fixed X (X > 1) and Y (Y ≥ 0) the program should establish

Looking at this program we realize that the number of times control goes through the loop equals the original value Y and we can ask ourselves whether we can speed things up. Well, the guarded command has now the task to bring y down to zero: without changing the value of h , we can investigate whether we can change the representation of that value, in the hope of decreasing the value of y . We are just going to try to exploit that the concrete representation of a value of h as given by x^y is by no means unique. If y is even we can halve y and square x, and this will not change h at all. Just before the squeezing operation we insert the transformation towards the most attractive representation of h and here is the next program:

I have included this example for various reasons. The discovery that a mere insertion of what on the abstract level acts like an empty statement could change an algorithm invoking a number of operations proportional to Y into one invoking a number of operations only proportional to log(Y) startled me when I made it. This discovery was a direct consequence of my forcing myself to think in terms of a single abstract variable. The exponentiation program I knew was the following:

Seventh example,

For a fixed value of n (n ≥ 0) a function f(i) is given for 0 ≤ i < N . Assign to the boolean variable “allsix” the value such that eventually

By the time that we read this program —or perhaps already earlier— we should get the uneasy feeling that as soon as a function value ≠ 6 has been found, there is not much point in going on. And indeed, although (P and j = n) ⇒ R , we could have used the weaker

Exercise. Give for the same problem the correctness proof for

Eighth example.

Before I can state our next problem, I must first give some definitions and a theorem. Let p = (p₀, p₁, ... , p_n-1) be a permutation of n (n > 1) different values p_i (0 ≤ i < n), i.e. (i ≠ j) ⇒ (P_i ≠ P_j) . Let q = (q₀, q₁, ... , q_n-1) be a different permutation of the same set of n values. By definition “permutation p precedes q in the alphabetic order” if and only if for the minimum value of k such that p_k ≠ q_k we have p_k < q_k .

The so-called “alphabetic index_n” of a permutation of n different values is the ordinal number given to it when we number the n! possible permutation arranged in alphabetic order from 0 through n!-1 For instance, for n = 3 and the set of values 2, 4 and 7 we have

Let (p₀§ p₁§ ... §p_n) denote the permutation of the n different values in monotonicly increasing order, i.e. index_n((p₀§ p₁§ ... §p_n)) = 0. (For example (4§ 7§ 2) = (2, 4, 7) but also (7§ 2§ 4) = (2, 4, 7) .)

With the above notation we can formulate the following theorem for n > 1:

After these preliminaries we can describe our problem. We have a row of n positions (n > 1) numbered in the order from left to right from 0 through n-1 ; in each position lies a card with a value written on it such that no two different cards show the same value.

When at any moment c_i (0 ≤ i < n) denotes the value on the card in position i , we have initially

In order to perform this transformation we must find a class of states —all satisfying a suitable condition P1— such that both initial and final states are specific instances of that class. Introducing a new variable, s say, an obvious candidate for P1 is

Again we ask, whether we can think of restricting the range of s and in view of its initial value we might try

Our next concern is, what to choose for “a suitable amount”. Because our increase of s must be accompanied by a reaarngement of the cards in order to keep P1 invariant, it seems wise to investigate whether we can find conditions, under which a single cardswap corresponds to a known increase of s . Let for a value of k satisfying 1 ≤ k < n hold

I therefore suggest to strengthen our original invariant relation P1 with the additional relation P2 —fixing the function of a new variable k —

In order to find “the suitable amount” for a major step the machine first determines the largest smaller value of k for which r < s + k! no longer holds — c_i with i = n-k-1 is then too small, but to the left of it they are all OK— and then increase s by the minimum multiple of k! needed to make r < s + k! hold again; this is done in “minor steps” of k! at a time, simultaneously increasing c, with cards to the right of it. In the following program we introduce the additional variable kfac , satisfying

Transcribed by Martin P.M. van der Burgt
Last revision 2014-11-15 .