Scott Burson  <FSet.SLB@gmail.com> wrote:
+---------------
| rpw3@rpw3.org (Rob Warnock) wrote:
| > Specifically, proving loop
| > termination involve searching for a loop invariant predicate
| 
| You have put your finger on the problem.  Most interesting proofs of
| program properties involve invariants (loop invariants, recursion
| invariants, class invariants, module invariants, etc.).  And as you
| note, there is no procedure for extracting an invariant from a piece
| of code; humans evidently do it through some combination of experience
| and explicit search, and no one has managed to automate it.
+---------------

Though note that in the case of the Dijkstra/Gries formalism, one
is *NOT* trying to "extract an invariant from a piece of code" per se.
The code hasn't been written yet, and *won't* be until the desired
invariant has been found. Rather, the task is to extract an invariant
from the post-condition of the loop, one which produce an acceptable
pre-condition on the loop which makes progress towards the ultimate
pre-condition of "NIL". Then once a usable loop invariant predicate
is found, the writing of the loop code -- and simultaneous proof of
same -- is trivial (at least by comparison).

This is not just a quibble, but is a fundamental difference in approach.
People who have not grokked that part fully seem to think that that in
the Dijkstra/Gries formalism one still "writes a little bit of code and
then somehow tries to prove it", which is absolutely incorrect. Instead,
one constructs a little theorem (or lemma), whereupon the code corresponding
to that proof is immediately manifest, since the coding primitive are
*defined* as "predicate transformers" when take a post-condition predicate
and transformer it into a pre-condition predicate.

Tiny, tiny example -- given the following pre-condition & post-condition:

    (assert (= x 3))          ; pre-condition
    ...[what code goes here?]...
    (assert (= x 17))         ; post-condition

we search for a predicate transformer that will transform (= X 17)
to (= X 3). By inspection, we see that the latter is equivalent
to (= X (- 17 14)), so that the predicate transformer we seek is
one that will change any post-condition (= X Y) into (= X (- Y 14)).
The code (INCF X 14) is such a predicate transformer, that is:

   Wp((= X Y), (INCF X 14)) ==> (= X (- Y 14))

[where "Wp" is the "Weakest pre-condition" operator, which takes
a post-condition and an imperative action (code) and returns the
weakest pre-condition that must be true for the post-condition to
be true following the action] and we immediately see that it satisfies
the proof:

    (assert (= x 3))          ; pre-condition
    (incf x 14)
    (assert (= x 17))         ; post-condition

Anyway, sorry for the sledghammer overkill, but I cannot stress
enough that in the Dijkstra/Gries formalism one is *never*
"proving the code"; instead, the proof *writes* the code.

Of course, that doesn't relieve the fact that *finding* the proof
[especially in the case of loops] is not the hard part...  ;-}

+---------------
| > Still, I suspect that creating an "expert system programming assistant"
| > to help programmers find appropriate loop invariant predicates using
| > Dijkstra's formalism would, in the long run, be a more effective use
| > of resources than continuing to beat our heads against the *known*
| > incomputable wall of "write it first *then* try to prove it".
| 
| I actually believe it to be the same problem, in essence.  If you can
| find the invariants, you've solved the problem of searching in these
| high-branching-factor spaces, and the rest of the proof problem will
| yield to the same techniques.
+---------------

Yup. Just so!


-Rob

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