Newsgroups: comp.lang.misc
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!van-bc!ubc-cs!uw-beaver!june.cs.washington.edu!pattis
From: pattis@june.cs.washington.edu (Richard Pattis)
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr14.001657.22816@beaver.cs.washington.edu>
Sender: news@beaver.cs.washington.edu (USENET News System)
Organization: Computer Science & Engineering, U. of Washington, Seattle
References: <12APR91.20195376@uc780.umd.edu> <1991Apr13.165135.7820@watmath.waterloo.edu> <13APR91.15060840@uc780.umd.edu>
Date: Sun, 14 Apr 91 00:16:57 GMT

In article <13APR91.15060840@uc780.umd.edu> cs450a03@uc780.umd.edu writes:
>Michael Coffin writes:
>>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]"
>>
>>...  It's quite different to point to a routine for quicksort and
>>claim that the partitions and exchanges somehow describe
>>"sortedness."
>
>But it is not all that different to point to a routine for bubble-sort
>and claim that the comparisons and exchanges somehow describe
>"sortedness".
>
>Assuming that A can be ordered.
>
>Raul

I always use this specification in class and ask whether it is a necessary
and sufficient condition to ensure their intuitive notion of what a sorting
subprogram should do.  Pretty much everyone agrees that this just about says
it all.  Then I show them a "sorting" subprogram that sets each element,
A[i], to the value i.  Sure enough, it satisfies the postconditions. There is
silence, then everyone starts to yell that the question was unfair since it
was "obvious" that I also meant the output was a permutation of the input.
Then we talk about "obvious", "proof", and some other things. Finally, we go
on to try to write code that correctly checks permutations, which itself gets
hairy.

  I know the definition above didn't quite say that it was the correct
postcondition for a sort subprogram, it just describes what ordered
means (and if checked by code that directly implements the "logic", will
require n**2 operations, because there are n**2 pairs of i,j).

Also, it might be better to write

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

Most of my students (freshman) don't know about partial orders, so
they see little difference between the two descriptions.

Rich Pattis
-- 
------------------------------------------------------------------------------
  Richard E. Pattis			"Programming languages are like
  Department of Computer Science	 pizzas - they come in only "too"
    and Engineering			 sizes: too big and too small."