``` Subject: Re: Can you learn computer science from a school? From: rpw3@rpw3.org (Rob Warnock) Date: Sun, 20 May 2007 00:19:16 -0500 Newsgroups: comp.lang.lisp Message-ID: <C6udnQI_m6bJR9LbnZ2dnUVZ_umlnZ2d@speakeasy.net> ```
```John Thingstad <john.thingstad@chello.no> wrote:
+---------------
| Larry Clapp <larry@theclapp.org> wrote:
| > This sounds very much like the philosophy behind Test Driven
| > Development.  ...
|
| For many practical applications it serves the same purpose.
| But a proof implies that given the precondition the specified
| operations make the postcondition a tautology. (always true)
| So you transform the precondition into the postcondition, so to speak.
| This is quite labor intensive and can to some extent be automated.
| (Isabelle, ACL2, etc)
+---------------

Yes, but in general, transforming the precondition into the
postcondition runs right into the Halting Problem!!  Whereas the
novel aspect of the Dijkstra/Gries methodology [to me, at least,
when I first read them] is that the identification for each imperative
construct of its corresponding "predicate transformer" allows one
to work in the *opposite* direction, more-or-less mechanically
transforming the postcondition back across the imperative step
into the precondition -- writing the code *backwards* from the
end -- in a much more deterministic fashion.

Of course, modulo the one difficulty that you [Thingstad] helpfully
reminded me of in your parallel reply, that of finding an appropriate
loop invariant to allow one to "back up" across a loop. That sometimes
does take a bit of head-scratching, and might be an area where some
automated assistance could help, I dunno.

+---------------
| Test cases are singular data-points and are not guarantied in general
| to cover the entire state space. So proof construction is considered
| more rigid. (It is still only as good as the assumptions in your
| pre and post conditions of cource.)
+---------------

I concur on both points.

-Rob

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

```