🚀 go-pugleaf

In article <12APR91.20195376@uc780.umd.edu> cs450a03@uc780.umd.edu writes:
>But if I have a routine called "sort" which sorts, and I feed a list
>into it which it can sort, the result is a sorted list.  Somebody has
>to establish that "sort" does indeed sort, but that would be true of a
>formal proof as well (you need to establish that you have a definition
>of "sorted" which fits within your formalism -- or else accept a
>priori that there is this thing called "sorted" and use its
>properties).

This is the whole point.  The definition of "sorted" can be translated
into a logical predicate pretty easily.  E.g., for a list of numbers
A, "A is sorted in ascending order" is translated to

    "for elements i and j in A, i <= j implies A[i] <= A[j]"

This is perhaps a leap of faith, but it's across a pretty narrow
canyon.  It's quite different to point to a routine for quicksort and
claim that the partitions and exchanges somehow describe "sortedness."

By the way, I agree with David Gudeman that proofs are prone to error.
But short of exhaustive testing, which is rarely possible, proofs are
the only way I know to reconcile the specification of a program with
its imperative realization.  It may not be particularly *good* tool, 
but as far as I can see it's the only tool.

Michael Coffin				mhcoffin@watmsg.waterloo.edu
Dept. of Computer Science		office: (519) 885-1211
University of Waterloo			home:   (519) 725-5516
Waterloo, Ontario, Canada N2L 3G1