About the presentation of programs (with A.J.M. van Gasteren)

A v G 2 / E W D 7 8 1 - 0

About the presentation of programs.

The purpose of this note is to explore a style of program presentation. Whenever we are aware of having adopted a convention, we shall describe and motivate it. We shall carry out our exploration by presenting a modest program. It is understood that this example will not confront us with all notational choices to be made - e.g. the example we have in mind doesn't call for the introduction of an abstract data type. We shall give, each time, a description, followed by an explanation of the conventions used, followed by a discussion of those conventions.

Our example is a program that we call binsrch embodying the idea of the binary search. Here is the specification of binsrch.

11 $N,X:$ int; M: array (0..N) of int; pres: bool{Qo: M(0) 5 X < M(N-1)}{Q1: (A i,j: 0 5 i s j < N: M(i) 5 M(j))}binsrch{pres such that R: pres= (Ei: 0 5 i < N: M(i) = X)}]

The explanation of the above is the following. The opening bracket "11" opens a scope, which the closing

bracket "Il" closes. The first three lines declare more or less in the style of PASCAL - why not?- the environment in which the more detailed speci- fication of binsrch is to be understood. In the text, binsrch is preceded by the precondition(s) and followed by the postcondition(s), conditions being surrounded by braces. This arrangement is deemed to prescribe for the program binsrch that initial satisfaction of the precondition(s) guarantees that activation of binsrch establishes the postcondition(s) in a finite number of steps; the "pres such that" in the postcondition indicates that R should be interpreted as am equation with pres as the unknown. Since part of the experiment is trying out the convention of in- dicating ranges of natural numbers with lower bound included but upper bound excluded, the subscript of M satisfies O's subscript $< N$ (hence the "more or less" in our reference to PASCAL). So much for the explanation; now the discussion.

ALGOL 60 uses the bracket pair "begin" "end" for different purposes : to form a compound statement and to delimit the scope of a nomenclature. We prefer to use different pairs for different purposes. Some programming languages indicate this difference by combining different opening brackets with one general closing bracket. Since reading program texts backwards should be per- missible, we are not attracted by that asymmetry.

Dedicated closing brackets are well-known, such as in "do...od" and "if...fo". From a lexical point of view, however, these "word delimiters" are unfortunate: one has to know them as bracket pairs and one has to know which one opens and which one closes. Since we never know how many bracket pairs we might need, we have chosen a way of generating them: a prefixed "[ " as opening bracket and a similarly postfixed ] " as the matching closing bracket. This is a perfectly general technique provided the square brackets are used for no other purpose. (We have considered the obvious alternative of the postfixed "[ " and the prefixed ]. Since the choice seemed technically irrelevant, we felt free to follow the tradition that started with the Kleene star.)

Note. We conclude that the sometimes adopted con- vention of delimiting comments by */ and */ is deplorable. (End of Note.)

Our convention of indicating a range of natural numbers from and including a lower bound up to and excluding an upper bound has been motivated elsewhere (see EWD768) and will not be discussed here.

In naming the declared variables we have adhered to our habit of using capital letters

for constants and lower-case letters for variables. Since a variable of a block can be a constant for one of its inner blocks, no attention should be paid to the distinction. Whether capital letters will be given a special role - such as, for instance, in the identifier "FirstElementInTheQueue" is still an open question. Two remarks, however, about the identifier pres , which is , of course, short for "present." The traditional name for such a boolean variable is "found" - often initialized with the value false !- , but for its operational connotations this name is most unfortunate. We have abbreviated "present" to the nonexisting word pres , thus avoiding ambiguity when referring to the variable in English prose. We -and not only we - have a strong suspicion that the use of mnemonic names is responsible for many errors in programming - the empty queue has no first element !- . The reason for not radically abolishing all mnemonic names is that in a sufficiently rigorous approach they should be harmless.

We have taken the somewhat oldfashioned view that a block primarily consists of declarations and statements, separated by semicolons, and that "comments" may be inserted where desired. This view explains the occurrence of the semicolons; in placing them at the beginnings of lines we have followed a suggestion of S.Doaifse Swierstra's.

A v g 2 / E W D 7 8 1 - 4

Thus the first column clearly reflects the syntactic structure of the block.

We have chosen to surround assertions by the traditional braces. Besides formulating the as- sertions we have named them for future reference; a further function of the closing brace is to mark the end of the formula named. Jux-ta-position of assertions denotes conjunction.

Note. The reader is invited to remember that this note discusses the presentation of programs rather than their development. The names Qo and Q1 are introduced separately because (we already know that) they are needed separately in the sequel. (End of Note.)

When an assertion need not be referred to we shall leave it anonymous. Occasionally -most likely for reasons of layout-the formulation of the assertion may be given outside the block.

The introduction of "such that" in the postcondition may amaze the reader. There were two reasons for not introducing a special character. Firstly, the most likely candidate, the colon, should not be overloaded too much; secondly -but time will show - we expect to need the "such that" so rarely that a special character would be inappropriate.

A v G 2 / E W D 7 8 1 - 5

We are left with the name binsrch ; it stands for the program to be presented in more detail in the sequel. That further presentation is to be un- derstood entirely within the context of the block we have given. ( Since this block is the universe of discourse for the remainder of the presentation, this block as a whole could remain anonymous.)

Our first block gives - in our current opinion - precisely what should be given first. It states the relevant conditions, the variables in which these are expressed are enumerated in the declarations, the proof obligations regarding binsrch follow from the structure of the text, and the names introduced give us the handles we need.

Our next task is to give a more detailed description of the statement birsrch. Here it is,

binsrch: int ${Q_0}$ $;10ct$ $Q_{2}:M(i)≤ X < M(i + 1)∧ O5i < N - 1}$ ${Q_1}$ $;pres:= (M(i) = X)$ ${R,seeNote1}$ ]

The purpose of the above is to introduce a local

integer variable i together with the full description of its role, i.e. to satisfy Q2 . The first line de- clares it, the next three lines give most of the func- tional specification of the statement loct -to be detailed later-. The next statement is not named but is fully given in situ. As before, the conditions surrounding it give its functional specification; since the statement is fully given, this is the moment to supply the argument that it, indeed, meets its func- tional specification. For this argument, the last line refers the reader to Note 1. Finally, the reader is supposed to convince himself that the above block meets the functional specifications of binsrch . So much for the explanation; now the discussion.

The above block is to be understood in the full context previously created for binsrch . This context includes the specification that within binsrch the identifiers $N,X,$ and M refer to constants; hence we have taken the liberty of not inserting "i such that" in front of "Q2". (Yet we feel free to insert such a phrase, though formally superfluous, when clarity seems to demand it.) This context also includes that ${Q_0\wedge Q_1}$ is the precondition of binsrch ; hence this precondition has not been repeated -say, between "binsrch : " and "I["- . Similarly, ${R} ^{\prime}$ has not been repeated after "J1". The place of the assertion " ${Q_{1}}"$ has been chosen for two reasons. Firstly, as time will show, loct does not need

A v G 2 / E W D 7 8 1 - 7

Q1 as a precondition for the establishment of Q2. Secondly, the second statement does need 01 for the establishment of R. Since we are describing, and not developing, a program, this is not the moment to prove the satisfiability of Q2: in due time the definition of loct will provide a constructive proof.

It is now time to give the still missing Note 1.

Note 1. The Axiom of Assignment tells us to prove

Q _ {1} \wedge Q _ {2} ⇒ (M (i) = X) = (E j: 0 ≤ j < N: M (j) = X).

In the case $M\left( i\right) = X$ ,this is obviously true. In the case $M\left( i\right) ≠ X$ ,we have,thanks to Q2, $M\left( i\right) < X < M\left( {i + 1}\right)$ ,and therefore,thanks to Q1, (A). $0 ≤ j < N : M\left( j\right) ≠ X)$ ,i.e. the truth of the right-hand side of the implication. We draw the reader's attention to the fact that this is the only place where we use ${Q}_{1}$ ,i.e. the fact that array $M$ is ordered. (End of Note 1.)

Our next task is to give a more detailed description of statement loct . Here it is.

A v G 2 / E W D 7 8 1 - 8

ct:|[j:int]

\begin{array}{l} i, j := 0, N - 1 \ {Q _ {3}: M (i) ≤ X < M (j) ∧ 0 ≤ i < j < N } \ \end{array}

; c l o s

{Q _ {3} ∧ i + 1 = j, h e n c e }

1

The purpose of loct was to assign to i a value satisfying Q2 , given the initial truth of Q0. The purpose of the above is to introduce a local nteger variable j, together with the full descrip- ion of its role . Its role is to satisfy Q3 to hart with and to satisfy eventually $c + 1 = j$ as well, so that Q2 is implied and can again be eliminated from the argument. The first statement, being given full, represents as before a proof obligation be fulfilled here and now; the absence of a reference to an explanatory "Note" means that this proof is entirely left to the reader. The fact that Q3 , the precondition of clos , is repeated in its postcondition states explicitly that Q3 is a so- called "invariant" for clos ; if clos turns out to be a repetition , $c + 1 = j$ will have to follow from the alsity of its guards. So much for the explanation. now the discussion.

We have not inserted " {Qo}" in front of the

A v g _ {2} / E w D 7 8 1 - 9

proof obligation, but the insertion would not have relieved the reader from consulting the context in which loct is to be understood (viz. the block called binsrch): he would have had to verify that the insertion was justified. For the same reason we have not inserted "Q2" after "hence". In the specification of clos we have stuck to our rule -to which we could adhere so far- of formulating postconditions as a single assertion. Note that this is the first case we encounter in which a postcondition could remain anonymous; this possibility is closely related to the decision not to repeat pre- and postconditions of statements in their refinements.

Our next task is to refine $\closeness$

\begin{array}{r l}{\mathrm {c l o s :}}&{\star [ i + 1 ≠ j}\&{\rightarrow \mathrm {I I} [ h: \mathrm {i n t} {j - i ≥ 2 }}\&{ ; \mathrm {a v e r} {h \mathrm {s u c h t h a t} i < h < j } {Q 3 }}\&{ ; - [ M (h) ≤ X \rightarrow i := h {Q 3, \underline {{i n c}} i }}\&{ ] \cdot X < M (h) \rightarrow j := h {Q 3, \underline {{d e c}} j }}\&{ ] - }\&{ ] | {Q 3, \underline {{d e c}} (j - i) }}\&{ ] *}\end{array}

The purpose of clos was to establish $i + 1 = j$ under invariance of Qs . We use the bracket pair "I" and "I" instead of the old "do...od" - to form a repetitive

construct. The repeatable statement is a block since it is the scope of the local integer constant h. The assertion j-iz2 being mentioned without referenceto an explanatory "Note",the reader is supposed to verify himself that it follows from the invariant and the guard. The role of constant h, which has mainly been introduced for brevity's sake, is to satisfy i< h< j. We use the bracket pair "[and]"- instead of the old "if...f-" to form an alternative construct. The absence of a reference to an explanatory "Note" in the final assertion leaves the reader with the obligation to verify that the block maintains the truth of Q3, that the block decreases the value of j-i and that the latter value is bounded from below. (The assertions following the alternatives can be viewed as hints towards this purpose.) So much for the explanation; now the discussion.

We have taken the liberty of placing assertions where we liked them. Similarly we have taken the liberly of writing simple guarded commands on single lines. We would like to stress that we have taken the position that the reader should be thoroughly familiar with the proof rules; the invariant relation and the con- vergence criterion - here denoted by "dec (j-i)"- have been given explicitly, since they are specific for this repetitive construct. The indication "dec (j-i)" is to be understood to refer to the complete pre-

A v g _ {2} / E W D 7 8 1 - 1 1

ceding guarded command of the repetitive con-Struct. Determining the "ranges" of the internal hints "inc i" and "decj", however, is left to the intelligent reader.

In a book presenting algorithms, the proof rules should be stated explicitly - in the introduction - for the sake of self-consistency of the text. They are so few and so ubiquitously used that explicit reference to them in the program presentations would be repetitious. In retrospect the explicit reference to the Axiom of Assignment in Note 1 was probably a mistake.

Our final task is the refinement of aver . We give three options :

aver: $h \mathrel{\text{:=}} i + 1$

$\overline{a}v\overline{e}r : h \mathrel{\text{:=}} j - 1$

$\operatorname{div}\left( {a + b}\right) = \operatorname{div}\left( a\right) - \operatorname{div}\left( b\right)$

Note 2. With div rounding to a nearest integer, aver establishes

2 \cdot h = i + j + d, \mathrm {w i t h} abs (d) ≤ 1.

Adding $j ≥ i + 2$ yields $2 \cdot h ≥ 2 \cdot i + 2 + d > 2 \cdot i$ , hence $i < h;h < j$ follows similarly from adding $i ≤ j - 2$ . (End of Note 2.)

We have given the different options for aver in order to show the extent to which the linear and the binary search can be mapped on each other. Note 2 has been given to stress this algorithm's independence of whether div rounds up or down. Our last refinement reveals another reason for introducing a name: "aver" had to be in-

Our presentation fails to express that only the first $N - 1$ elements of $M$ matter: the last element, which ,by definition,exceeds $X$ ,is never accessed and need not be stored. The coding trick,which we regret in retrospect,wouldn't have been necessary if we had replaced in Q3 the term $X < M\left( j\right)$

j = N - 1 \underline {{\underline {{c o r}}}} X < M (j)

The constant $N$ should have been chosen in such a way that the first $N$ elements of $M$ matter. In retrospect we feel that the introduction of the "plus infinity" at the far end of the array was a mistake.

When Wim Fegen saw our first pages, he was horrified by our choice of the identifier "binsrch".

It is indeed terrible: "bins" would have been less obnoxious. (We once erroneously wrote "binsearch" in full.) We then chose loct for locate, clos far close, and aver far average. Each time the choice of identifier was a pain in the neck; in contrast, the choice of the identifiers i, j, h, R, Q0, 01, Q2, and Q3 was absolutely painless. We now have the feeling that naming our statements, say, So, St, ek. would have been prefer- able.

We thank W.H.J. Fejen for a number of pertinent remarks while the above was being written.

Our final task is to solicit the reader's comments and advice.

16 March 1981

drs. A.J.M. van Gastoren BP Venture Research Fellow Department of Mathematics University of Technology 5600 MB EINDHOVEN The Netherlands

prof. dr. Edsger W.Dgksta Burroughs Research Fellow Plataanstraat 5 5671 AL NUENEN The Netherlands