Alan Crowe <alan@cawtech.freeserve.co.uk> wrote:
+---------------
| rpw3@rpw3.org (Rob Warnock) writes:
| > This is in fact what Dijkstra's "A Discipline of Programming"
| > or David Gries's "The Science of Programming" is all about:
| > a theory of abstraction...
| > For any serious professional programmer who has not read these,
| > I strongly recommend doing so. ...
| 
| I hope you are right because I have just bought myself a
| copy of A Discipline of Programming.
+---------------

Congratulations! I wasn't sure it was still in print.

+---------------
| [One] point I will be watching out for in my second attempt at
| reading the book is this:
| 
| It feels natural to say that this code is wrong
| 
|          (defun my-reverse (list)
|            (if (endp list)
|                nil
|                (append (my-reverse (rest list))
|                        (list (first list)))))
| 
| It is not enough that it gets the right answer, its
| extravagence disqualifies it. Dijkstra separates the concern
| about correctness from the concern about not using quadratic
| algorithms where linear ones are available.
| 
| Are the gains from separating these two concerns sufficient to
| repay the costs when the time comes to put them back together again?
+---------------

I *think* so. There's an old saying that "I can give you answers
as fast as you like, as long it you don't care if they're correct."
That's seldom what one really wants.

Rather, the usual advice is "First get it right, then make it fast".
Put in the context of the Dijkstra methodology, once you have a
correct solution *together* with it's embedded/intertwined proof,
then it's much easier to improve performance without breaking things
by making a series of proof-preserving transformations which preserve
the proof around the portion of code being transformed. Obviously,
some or even all of the internal proof may have to change with the
changed section of code, but the pre- & post-conditions *around*
the changes should survive.

Notice that I have not said how large a section of code is
appropriate for each such proof-preserving performance-enhancing
transformation. Unfortunately, that's *very* dependent on how
extensive the transformation needs to be to achieve the desired
performance improvement. Obviously, the larger the scope of each
"local" change, the harder it may be to prove that the change
preserves the important assertions around the periphery of the
changed portion.

The good news, such as it is, is that the Dijkstra proof methodology
is one of the few I've seen [though I'm certainly no expert in
program-proving methodologies!] which handles imperative constructs
[specifically, assignment] almost as conveniently as purely functional
constructs.


-Rob

-----
Rob Warnock			<rpw3@rpw3.org>
627 26th Avenue			<URL:http://rpw3.org/>
San Mateo, CA 94403		(650)572-2607