In 1968 the Communications of the ACM published a Letter to the Editor from E.W. Dijkstra (volume 11 (1968), pp 147–148). The Editor, perhaps a bit puzzled by the contents, summarized them by supplying as title “Goto Statement Considered Harmful”. The mere thought was sufficiently provocative to ensure that the idea spread like wildfire, initially to be dismissed, but soon to be blessed with universal approval. “Structured Programming” was born.

The most enthusiastic converts were the computer science professors. These people were doing research on esoteric topics like formal languages or graph theory and were press-ganged into teaching introductory programming. With little programming experience, they welcomed a clear rule (no GOTOs!) and reveled in the casuistry required for forcing non-conforming code into the straightjacket of the officially approved formats.

This essay is a thought experiment: suppose one had never heard of Structured Programming, that one wanted to solve a little programming problem by common sense reasoning; that this solution process not only had to supply the conviction of correctness, but also had to help discover the algorithm. My conclusion will be that these goals, though ambitious, are achievable, but that Structured Programming is at best a handicap.

Do I then conclude that Dijkstra was wrong in his Letter to the Editor? No, but I do conclude that one should not read as much into it as those in the Structured Programming mania have done. Dijkstra said that there is a positive correlation between the density of GOTOs and the density of bugs. I am prepared to believe that. He could have phrased it as “Lots of GOTOs — Lots of bugs.” He would then have echoed the rule “Bad spelling — bad thinking”, a rule that encapsulates the correlation observed by professors who have had to grade large numbers of student essays. The rule sounds provocative because the spelling and the thinking are at different levels. Surely, one can be a bad speller and a good thinker. Yes, that’s in theory. What the profs found in practice is that this theoretical possibility is rarely realized. What I hope this essay will convince you of is that Dijkstra’s Letter to the Editor has the same kind of validity as the rule “Bad spelling — bad thinking”. That, indeed, the more GOTOs in the source code (as typically found in 1968), the more bugs. This leaves open the possibility that a certain kind of thinking exists that leads to correct code in a process that ignores the precepts of Structured Programming.

#### The example

First some decisions: (1) What programming problem to solve for a demo? and (2) What language to use?

- For the problem I picked the partitioning stage in Hoare’s Quicksort. In practice I would not recommend Hoare’s partitioning algorithm: I would prefer Lomuto’s variant for the partitioning method as being easy to get right by conventional methods [1]. But for the present purpose I will pretend ignorance of Lomuto’s beautiful invention so that we will need to solve a problem that has been acknowledged as hard by Jon Bentley (“Programming Pearls”, Addison-Wesley, 1986, footnote on page 110):

Most presentations of Quicksort use a partitioning scheme based on two approaching indices, … . Although the basic idea of that scheme is simple, I have always found the details tricky — I once spent the better part of two days chasing down a bug hiding in a short partitioning loop. A reader of a preliminary draft complained that the standard two-index method is in fact simpler than Lomuto’s, and sketched some code to make his point; I stopped looking after I found two bugs.

It is unusual for a programmer to make such an admission, but then Bentley is an unusually good programmer. Another circumstance pointing to the selection of this task is that it has been selected by Hoare himself for his demonstration of formal verification (“Proof of a Program: FIND” by C.A.R. Hoare, Communications of the ACM, Vol. 14 (1971), pp. 39–45)

We are not about to code a pre-determined algorithm: more ambitiously, we start from a requirement. We end up with code that demonstrably satisfies it. Presumably there is an algorithm encoded in it, but we don’t need to know it as such. (Dijkstra does something similar with the examples in his book “A Discipline of Programming”.) An advantage of what follows here is that our code is more readily executable than that of Dijkstra’s book. Further description of the problem to be solved has to wait for a discussion of the next point.

- What language to use? Language is needed to describe the requirements of the function to be programmed and to carry out the reasoning that gives us our conviction of the program’s correctness. Both are informal. There is no dearth of formal approaches proposed in the course of decades of research. None of these has found any response among programmers. In addition to this difficulty there is the fact that software for formal verification is often more complex than the application to be verified and that the formal specifications are as hard to understand and get right as any code.

Formal specifications originate in informal notions. The goal of verification is conviction of correctness on the part of a responsible professional. This conviction is also informal. Thus we are going from informal to informal so that the use of formal verification is a detour. As it is not clear how such a detour would help, we aim at informal development leading to executable code and to conviction of its correctness with respect to an informal requirement. This informality does not preclude the use of algebraic notation referring to a mathematical model.

#### The computational model

The computational model is based on (computation) states; any state being determined by the values of the variables. (Computational) actions typically change a state. Actions are specified as binary relations, that is, as sets of pairs of states. A pair <s,t> is in the relation iff t is a possible state resulting from the action starting in state s. Binary relations include the identity relation consisting of the pairs <s,s> for all states s. We identify “action” with “binary relation over states” so that, paradoxically, there is an action that is the identity relation, that is, an action that does nothing. In addition, the actions include all subsets of the identity relation.

The composition of two actions X and Y is the action obtained by

executing Y in the state resulting from executing X. We write the

composition of X and Y as X;Y. Regarded as a binary relation, it is the set of all pairs <s,u> such that there is a state t with <s,t> in X and <t,u> in Y.

A set of states can be regarded as a condition by identifying the set with the condition that determines whether a state belongs to the set. Conditions define certain subsets of the identity relation: condition C defines the set of all <s,s> such that s belongs to C. For example, if x and y are variables, then x=y is a condition. If from the context it appears that x=y is a binary relation, then, for example x>y ; (x := y) is a binary relation, hence an action. It is an action that is only possible in a state that satisfies the condition x>y.

We will say “C-state” for a state satisfying condition C.

Conditions and actions are described by assertions and statements, respectively. We are interested in partially characterizing a statement by requiring that, if a state s satisfies assertion P, and statement S is possible and is executed starting from s, then there is a resulting state that satisfies assertion Q. Let us call this relationship between P, S, and Q a *triple*. Hoare used the notation {P}S{Q}. We may regard S as a non-deterministic operator on states. From this point view there is a similarity between triples and the quantum-mechanical objects denoted by Dirac’s notation <Q|S|P>, where the Q part is called “bra” and the P part is called “ket”. As there will be no confusion with quantum mechanics, we will write {P}S{Q} as <P|S|Q>. That is, we adopt the bars and angled brackets from Dirac, but we stick to the order in which the input is on the left and the output on the right. Although we are just using a superficial similarity between the quantum mechanical notion and Hoare’s triple, we don’t want to rule out the possibility of something deeper, like a common generalization.

#### Analysis

Our goal is to write a function body that executes the partition phase of Quicksort. The function body is a statement, probably compound, that we call S. It needs to satisfy <P|S|Q> where condition P is:

indexes p and q bound a segment of a numerical array a and p < q

We denote the sequence a[p],…,a[q] as a[p..q].

We write e.g. a[p..i-1] <= m for

for all x, p <= x < i implies a[x] <= m

There is available a function with heading

void swap(int a[], int x, int y)

that interchanges the values of a[x] and a[y].

The purpose of S is to execute calls to swap() and to find an index j such that the state satisfies the condition Q, which is:

p <= j <= q and a[p..j-1] <= a[j] and a[j+1..q] >= a[j]

Moreover, in the final state a[p..q] should be a permutation of a[p..q] in the initial state. As the only changes to the content of a[p..q] will be calls to swap(), this is automatically satisfied. Accordingly, there will be no need to include the permutation requirement in any of the assertions.

It would be nice if we would see right away a simple statement S such that <P|S|Q>. As this is not the case, we look for an intermediate condition I such that <P|S0|I> and <I|S1|Q> with simple S0 and S1. This comes down to finding I as a common generalization of P and Q. One such I is:

a[p] = m and p < i and i <= k+1 and k < q and a[p..i-1] <= m and a[k+1..q] >= m

It may help to draw diagrams for Q and for I.

An S0 satisfying <P|S0|I> is

if (a[p] > a[q]) swap(a,p,q); m = a[p]; i = p+1; k = q;

We don’t see a simple S1 to satisfy <I|S1|Q>, so we postulate an intermediate I0 such that <I0|S10|Q>. If we define I0 as (I & i >= k) then S10 can be

if (a[i] > m) j = i-1; // a[j] <= m & a[j+1..q] >= m swap(a,p,j); return j;

In (I & i >= k) we have k <= i <= k+1, so that i is k or k+1. That is, a[p..i-1] and a[k+1..q] touch or have a single element in between. Again, a diagram may help.

We now have the triples <P|S0|I> and <I0|S10|Q>. If we would have (I => I0), then we could conclude <P|S0;S1|Q> and partitioning would be solved by the program S0;S1. That not being the case, we look for a statement X such that <I|X|I0>. If we define I1 as I & i<k then we can find an X such that <I|X|(I0 or I1)>. As execution of X may result in an I1-state and I1 does not imply Q, we need a triple with I1 as pre-condition and Q, I1, or I0 as post-condition. A promising triple is <I1|Y|I>, with Y equal to

if (a[i] <= m) i++; else if (m <= a[k]) k--; else {swap(a,i,k); i++; k--;}

Our triples are now

<P|S0|I> <I|X|(I0 or I1)> <I0|S10|Q> <I1|Y|I>

In a sense these triples solve the partitioning problem. S0 terminates from any P-state and similarly for the triples containing S10 and Y. We haven’t seen X yet, but it will terminate for any I-state. All triples together determine that, for any P-state, one of the sequences

S0 X (Y X)* S10

performs partitioning. The number of occurrences of Y is finite because Y increases i or decreases k and neither can do so indefinitely.

#### Synthesis

Though the triples are not executable, they are easily translated to executable code. A triple <A|S|B> translates to

A: S; goto B;

in the C programming language.

We haven’t written yet written the X in <I|X|(I0 or I1)>. In general, a triple <A|S|AB0 or AB1>, where AB0 is (A and not B) and AB1 is (A and B), is satisfied when S is

if (B) goto AB1; else goto AB0;

The translations of the triples should be preceded by

goto P;

and followed by

Q: return ...;

In this way we get as a translation of the triples for partitioning:

goto P; /////triple:///// I: if (i >= k) goto I0; else goto I1; /////triple:///// I0: j = (a[i] > m) ? i-1 : i; swap(a,p,j); goto Q; /////triple:///// I1: if (a[i] <= m) i++; else if (m <= a[k]) k--; else {swap(a,i,k); i++; k--;} goto I; /////triple:///// P: if (a[p] > a[q]) swap(a,p,q); m = a[p]; i = p+1; k = q; goto I; ///////////////// Q: return j;

The validity of the triples ensures that when this is executed starting from a P-state, the resulting state (if any) is a Q-state. There *will* be a resulting state is guaranteed, among other things, by the fact that Y is executed a finite number of times.

Just as there is no order among the triples, the order among their translations is immaterial. But certain orders allow more optimization. The above can be re-ordered and optimized to:

if (a[p] > a[q]) swap(a,p,q); m = a[p]; i = p+1; k = q; I: if (i >= k) goto I0; if (a[i] <= m) i++; else if (m <= a[k]) k--; else {swap(a,i,k); i++; k--;} goto I; I0: j = (a[i] > m) ? i-1 : i; swap(a,p,j); return j;

#### Comparison with Structured Programming

This latter program is not suitable for human consumption. This short partitioning loop could easily hide a bug like the one that gave Bentley so much trouble. If only P and Q were given and if this program were presented as an S to satisfy <P|S|Q>, then the assertions would have to be discovered — the notoriously difficult program verification problem. But in the process described here the assertions were there first, suggested by the specification, jointly with the triples. The programmer can think in terms of assertions and triples, not branches and loops. Compared with this process, let’s call it *Assertion-Driven Programming*, Structured Programming is a distraction and a handicap, an artificial restriction to the use of canned branches and loops.

Assertion-Driven Programming is not the coding of an *algorithm*. Yet, in this case, the end product behaves like Hoare’s partitioning algorithm rather than Lomuto’s. Somewhere along the line a decision must have been taken that caused Hoare’s algorithm to come out. This choice is a consequence of the choice of I as an assertion intermediate between P and Q. The intermediate chosen here is not the only one possible; there is some other one that would have led to Lomuto’s algorithm.

Let’s represent the unordered collection of triples by a labeled graph. This has the advantage that we can relate Assertion-Driven Programming to Structured Programming. In this graph representation the assertions are the nodes; the triples are the directed edges, with the actions labeling these edges. The computations are paths from P to Q. Of course these paths can be described by a regular expression. The operators of regular expressions are similar to the Structured Programming constructs: star is like while; plus is like if-then-else.

Which is better: the regular expression or the graph? In the graph the vertices are explicit; they correspond to the assertions. The regular expression hides this information. To end up with verified code, we need to start with the assertions, which makes the graph essential. This explains the superiority of Assertion-Driven Programming over Structured Programming.

The assertions are informal. The computational model is mathematically sketchy. These shortcomings are an essential advantage: Assertion-Driven Programming is intended to help a practicing programmer to write correct code. Far from being contradictory, testing of the final product is essential: nothing real is error-free right away. But debugging in Assertion-Driven Programming is different. It does not address the executable code, but it requires the programmer to re-start the entire Assertion-Driven process: to check the assertions, the validity of the triples, and the transcription to executable.

#### Summary

In Assertion-Driven Programming one starts with a specification in terms of a precondition P and a postcondition Q. These provide the initial assertions. Usually it is not immediately clear which sequence S of statements satisfies the triple.

Intermediate assertions are suggested by the existing ones to make it more likely that the required bridging statements can be found. As soon as the assertions and the triples guarantee that there is a computation from any P-state to a Q-state, the set of triples is complete. The triples are then transcribed to executable code.

#### PS

There is more in Dijkstra’s letter than the observation that the densities of GOTOs and of bugs are positively correlated. Of course, neither Dijkstra nor his any of his readers will have made the mistake of concluding a causal relationship one way or the other. In his letter, Dijkstra also observed that the human mind is bad at visualizing processes evolving in time, so that it is safer to think in terms of static relationships. Structured Programming still refers to a dynamic model; its advantage is that the dynamic model is simpler. Assertion-Driven Programming takes a more drastic step towards a static model.

#### Notes

[

May 23, 2009 at 6:42 pm |

The idea of programs as transformations or operators from state to state, where states are described by a set of assertions is very interesting. We need to look at more extended examples, and see what operations are possible for two triples, other than composition as shown in the given example. The link to structured programming and goto’s is I think less significant and less interesting, in fact somewhat distracting the basic idea

March 12, 2016 at 11:00 pm |

I have had a lot of success with the coding style demonstrated in your article, because it is a much more effective and reliable way to express a state machine than with if, then, else, which often misses key states and is not easy to grasp. As with so many pursuits, one needs to find the best tool for the job.

I am much intrigued by the mathematical process that you have described for discovering the required state machine. Thank you.