Scott Burson <FSet.SLB@gmail.com> wrote:
+---------------
| Halting Problem says that termination is uncomputable: that there is
| no algorithm that can tell you, for every program P, whether P
| terminates. Yet proofs of termination of particular algorithms are a
| staple of CS work. So if the specification of a program includes the
| statement that the program terminates -- which is certainly a well-
| defined property -- then proving that the program meets that aspect of
| the specification, while clearly possible in almost all cases of
| interest, is uncomputable. So there is _some_ formal method of
| proving that the program has this property; it's just not a method
| that we know how to automate (well enough to be generally useful).
+---------------
The situation is neither as dire *nor* as favorable as many who argue
the extremes may wish to portray. If you're given a random program
and asked to prove whether or not it conforms to some other random
specification -- even as simple as "it terminates" -- then, yes, this
is uncomputable *in general*. However, individual program instances
*might* be provable. You just don't know which ones until you try
[and your proof system either terminates... or doesn't].
The real problem, IMHO, is that we have all [well, mostly all] been
ignoring the advice of people like Dijkstra & Gries &c. who recommend
abandoning the whole "try to prove that program A meets spec B" approach,
and instead suggest growing the program *and* the proof *together* from
the spec, using "predicate transformers" to work backwards in a formal,
provable manner from the desired results [the "post-conditions"] to the
specified initial conditions [the "pre-conditions"]. There is no issue
of computability with the approach, since at no time is the program that's
being constructed allowed to contain unprovable elements. Dijkstra's
famous monograph on this approach is called "A Discipline of Programming":
http://www.amazon.com/dp/013215871X
Gries's later textbook, which might be more approachable to many, is
called "The Science of Programming":
http://www.springer.com/computer/programming/book/978-0-387-96480-5
http://www.amazon.com/dp/0387964800
But to bring my diversion back on-topic, the theoretical problem with
the Dijkstra/Gries approach is that the technique is not constructive,
and hence cannot be (fully) automated. Specifically, proving loop
termination involve searching for a loop invariant predicate that meets
the pre- & post-conditions [less the termination condition] *and* "makes
non-zero progress" [typically decrements a positive number, where said
number being zero is the termination condition]. Once you have found
some appropriate loop invariant predicate, the proof of correctness
and termination of the loop is trivial [and is trivially automatable].
Unfortunately, their formal method doesn't help you at all in *finding*
such a predicate!! All one has available for guidance is "style",
"experience", "heuristic", etc.
[One is reminded of Shannon's famous Coding Theorem, which proves that,
given some specific channel, a block code exists that can produce throughput
"as close as you like" to the theoretical maximum information carrying
capacity of the channel with, at the same time, an error rate "as low
as you like"... but does not provide *any* guidance as to how to *find*
such a block code!! (*sigh*)]
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".
-Rob
-----
Rob Warnock <rpw3@rpw3.org>
627 26th Avenue <URL:http://rpw3.org/>
San Mateo, CA 94403 (650)572-2607