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