Dijkstra was not insane
Recently, a reader on the Higher-Order Perl
discussion mailing list made a remark about Edsger Dijkstra and
his well-known opposition to the break construction (in Perl,
last) that escapes prematurely from a loop. People often use
this as an example to show that Dijkstra was excessively doctrinaire,
and out of touch with the reality of programming[1], but usually it's
because they don't know what his argument was.
I wrote a response, explaining where Dijkstra was coming from, and I
am very happy with how it came out, so I'm reposting it here.
The list subscriber said, in part:
On a side note, I never read anything by Dijkstra that wasn't noticeably
out of touch with the reality of programming, which qualifies them as
screeds to me.
And I say that as a former Pascal programmer, and as one who has read,
and bought into, things like Kernighan's "Why Pascal is Not My Favorite
Programming Language" and the valid rants about how some form of
breaking out of a loop without having to proceed to the end is very
useful, without destroying structure (except by Dijkstra's definition of
structure)...
A lot of people bring up the premature-loop-exit prohibition without
understanding why Dijkstra suggested it; it wasn't just that he was a
tightassed Dutchman.
Dijkstra's idea was this: suppose you want to prove, mathematically,
that your program does what it is supposed to do. Please, everyone,
suspend your judgment of this issue for a few paragraphs, and bear
with me. Let's really suppose that we want to do this.
Dijkstra's idea is that the program is essentially a concatenation of
blocks, each of which is trying to accomplish something or other, and
each of which does not make sense to run unless some part of the
program state is set up for it ahead of time. For example, the
program might be to print a sorted list of links from a web page.
Then the obvious blocks are:
- A
- get the web page and store it in a variable
- B
- extract the links from the text in the variable into an array
- C
- sort the array
- D
- print out the array contents
Section C is trying to sort the array; if it is correct then the array
will be sorted by the time step D commences. But it doesn't make
sense to commence step C unless the array is populated. Garbage in,
garbage out, as they used to say when I was in elementary school.
We say that the "precondition" for C is that the array be populated
with URLs, and the "postcondition" is that the array be in sorted
order. What you would want to prove about C is that if the
precondition holds—that is, if the array is properly populated
before C begins—then the postcondition will hold too—that is, the
array will be in sorted order when C completes.
It occurs to me that calling this a "proof" is probably biasing
everyone's thinking. Let's forget about mathematical proofs and just
think about ordinary programmers trying to understand if the program
is correct. If the intern in the next cubicle handed you his code for
this program, and you were looking it over, you would probably think
in very much this way: you would identify block C (maybe it's a
subroutine, or maybe not) and then you would try to understand if C,
given an array of URLs, would produce a properly sorted array by the
time it was done.
C itself might depend on some sub-blocks or subroutines that performed
sub-parts of the task; you could try to understand them similarly.
Having proved (or convinced yourself) that C will produce the
postcondition "array contains sorted list of URLs", you are in an
excellent position to prove (or convince yourself) that block D prints
out a sorted array of URLs, which is what you want. Without that
belief about C, you are building on sand; you have almost nothing to
go on, and you can conclude hardly anything useful about the behavior
of D.
Now consider a more complex block, one of the form:
if (q) { E; }
else { F; }
Suppose you believe that code E, given precondition x, is
guaranteed to produce postcondition y. And suppose you believe
the same thing about F. Then you can conclude the same thing about
the entire if-else block: if x was true before it began
executing, then y will be true when it is done.[2] So you can build up proofs (or beliefs)
about small bits of code into proofs (or beliefs) about larger ones.
We can understand while loops similarly. Suppose we know that
condition p is true prior to the commencement of some loop, and that
if p is true before G executes, then p will also be true when G
finishes. Then what can we say about this loop?
while (q) { G; }
We can conclude that if p was true before the loop began, then p will
still be true, and q will be false, when the loop ends.
BUT BUT BUT BUT if your language has
break, then that guarantee goes out the window and you can
conclude nothing. Or at the very least your conclusions will become
much more difficult. You can no longer treat G atomically; you have
to understand its contents in detail.
So this is where Dijkstra is coming from: features like break[3]
tend to sabotage the benefits of structured programming, and prevent
the programmer from understanding the program as a composition of
independent units. The other subscriber made a seemingly disparaging
reference to "Dijkstra's idea of structure", but I hope it is clear
that it was not an arbitrary idea. Dijkstra's idea of structure is
what will allow you to understand a large program as a collection of
modules.
Regardless of your opinion about formal verification methods, or
correctness proofs, or the practicality of omitting break
from your language, it should at least be clear that Dijkstra was not
being doctrinaire just for the sake of doctrine.
Some additional notes
Here are some interesting peripheral points that I left out of my
main discussion because I wanted to stick to the main point, which
was: "Dijkstra was not insane".
- I said in an earlier post that "I often find
Dijkstra's innumerable screeds very tiresome in their unkind,
unforgiving, and unrealistic attitudes toward programmers." But
despite this, I believe he was a brilliant thinker, and almost every
time he opened his mouth it was to make a carefully-considered
argument. You may not like him, and you may not agree with him, but
you'll be better off listening to him.
An archive of Dijkstra's
miscellaneous notes and essays (a pre-blogging blog, if you like)
is maintained at the University of Texas. I recommend it.
- I said:
if (q) { E; }
else { F; }
Suppose you believe that code E, given precondition x,
is guaranteed to produce postcondition y. And suppose you
believe the same thing about F. Then you can conclude the
same thing about the entire if-else block.
Actually, your job is slightly easier. Let's write this:
[x] E [y]
to mean that code E, given precondition x, produces postcondition
y. That is, if we know that x is true when E begins execution,
then we know that y is true when E finishes. Then my quoted
paragraph above says that from these:
[x] E [y]
[x] F [y]
we can conclude this:
[x] if (q) {E} else {F} [y]
But actually we can make a somewhat stronger statement. We can
make the same conclusion from weaker assumptions. If we believe these:
[x and q] E [y]
[x and not q] F [y]
then we can conclude this:
[x] if (q) {E} else {F} [y]
In fact this precisely expresses the complete semantics of the
if-else construction. Why do we use if-else blocks anyway? This
is the reason: we want to be able to write code to guarantee
something like this:
[x] BLAH [y]
but we only know how to guarantee
[x and q] FOO [y]
and
[x and not q] BAR [y]
for some q. So we write two blocks of code, each of which
accomplishes y under some circumstances, and use if-else to make
sure that the right one is selected under the right circumstances.
- Similar to break (but worse), in the presence of goto you are
on very shaky ground in trying to conclude anything about whether
the program is correct. Suppose you know that C is correct if its
precondition (an array of URLs) is satisfied. And you know that B
will set up that precondition (that is, the array) if its
precondition is satisfied, so it seems like you are all right. But
no, because block W somewhere else might have goto C; and
transfer control to C without setting up the precondition, and
then C could cause winged demons to fly out of your nose.
Further reading
-
For a quick overview, see the Wikipedia article
on Hoare logic. Hoare logic is the
[x] E [y] notation I used above, and a set of
rules saying how to reason with claims of that form. For example,
one rule of Hoare logic defines the meaning of the null statement: if ; is the null
statement, then [p] ; [p] for all conditions
p.
Hoare logic was invented by Tony Hoare, who also invented the
Quicksort algorithm.
-
For further details, see Dijkstra's book "A Discipline of
Programming". Dijkstra introduces a function called wp for
"weakest precondition".
Given a piece of code C and a desired postcondition
q, wp(C, q) is the weakest precondition
that is sufficient for code C to accomplish q. That
is, it's the minimum prerequisite for C to accomplish
q. Most of the book is about how to figure out what these
weakest preconditions are, and, once you know them, how they can
guide you to through the implementation of your program.
I have an idea that the Dijkstra book might be easier to follow after
having read this introduction than without it.
- No discussion of structured programming and goto is
complete without a mention of Donald Knuth's wonderful paper
Stuctured Programming with go to Statements.
This is my single all-time favorite computer science paper. Download it here.
- Software Tools in Pascal is a book by Kernighan and
Plauger that tries to translate the tool suite of their earlier
Software Tools book into Pascal. They were repeatedly
screwed by deficiencies in the Pascal language, and this was the
inspiration for Kernighan's famous "Why Pascal is not my Favorite
Programming Language" paper. In effect, Software Tools in
Pascal is a book-length case study of the deficiencies of
Pascal for practical programming tasks.
[Other articles in category /prog]
permanent link
|