Subject: Re: Can you learn computer science from a school?
From: (Rob Warnock)
Date: Sun, 20 May 2007 00:19:16 -0500
Newsgroups: comp.lang.lisp
Message-ID: <>
John Thingstad <> wrote:
| Larry Clapp <> 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 Warnock			<>
627 26th Avenue			<URL:>
San Mateo, CA 94403		(650)572-2607