Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!udel!haven!ni.umd.edu!uc780.umd.edu!cs450a03
From: cs450a03@uc780.umd.edu
Newsgroups: comp.lang.misc
Subject: RE: Formal definitions (Re: ada-c++ productivity)
Message-ID: <13APR91.15060840@uc780.umd.edu>
Date: 13 Apr 91 15:06:08 GMT
References: <11APR91.19210188@uc780.umd.edu> <1991Apr12.125553.7307@watmath.waterloo.edu> <12APR91.20195376@uc780.umd.edu> <1991Apr13.165135.7820@watmath.waterloo.edu>
Sender: usenet@ni.umd.edu (USENET News System)
Organization: The University of Maryland University College
Lines: 18
Nntp-Posting-Host: uc780.umd.edu

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