Newsgroups: comp.lang.misc
Path: utzoo!utgpu!watserv1!watmath!tolstoy.waterloo.edu!mhcoffin
From: mhcoffin@tolstoy.waterloo.edu (Michael Coffin)
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr13.165135.7820@watmath.waterloo.edu>
Sender: news@watmath.waterloo.edu (News Owner)
Organization: University of Waterloo
References: <11APR91.19210188@uc780.umd.edu> <1991Apr12.125553.7307@watmath.waterloo.edu> <12APR91.20195376@uc780.umd.edu>
Date: Sat, 13 Apr 1991 16:51:35 GMT
Lines: 29

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