```
Subject:
```**Re: PLOT: A non-parenthesized, infix Lisp!**

From: rpw3@rpw3.org (Rob Warnock)

Date: Mon, 04 May 2009 00:19:02 -0500

Newsgroups: comp.lang.lisp,comp.lang.misc,comp.lang.scheme

Message-ID: <oOKdnTL62spb52PUnZ2dnUVZ_uydnZ2d@speakeasy.net>

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