John Thingstad <firstname.lastname@example.org> wrote:
| Larry Clapp <email@example.com> 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 <firstname.lastname@example.org>
627 26th Avenue <URL:http://rpw3.org/>
San Mateo, CA 94403 (650)572-2607