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: <1991Apr12.125553.7307@watmath.waterloo.edu>
Sender: news@watmath.waterloo.edu (News Owner)
Organization: University of Waterloo
References: <1755@optima.cs.arizona.edu> <1991Apr11.214018.19443@watmath.waterloo.edu> <11APR91.19210188@uc780.umd.edu>
Date: Fri, 12 Apr 1991 12:55:53 GMT
Lines: 34

In article <11APR91.19210188@uc780.umd.edu> cs450a03@uc780.umd.edu writes:
>eh?  imperative programming languages don't say "achieve this goal" ?

No.  Imperative languages specify a series of actions, not the results
of those actions.  Some imperative languages have assertions, which
look as though they specify results, but they're interpreted as as
run-time checking: if this isn't true, print an error message or raise
an exception.

>I mean, if I say "sort this list" that's the sort of thing that an
>imperative language does.  That's an equivalent statement to "make
>this list sorted".

But neither is equivalent to "this list IS sorted", which is what
proofs allow you to say, and which is the way the specification of the
sorting program is probably phrased.  The closest you can get in an
imperative language is saying "Check whether the list is sorted; if it
isn't, abort the program or raise an exception".

>Maybe you don't like the levels of abstraction available to you in
>some imperative languages?

No, I do like them, but they don't provide the same things as do
proofs.  Encapsulating in a procedure named "sort" all the swaps that
accomplish sorting just pushes the problem down a level.  The question
remains: how do I know that after calling "sort(x)" the array x is
sorted?  Well, I can either test the routine "sort", or I can prove
that after calling it the array will be sorted.  Which to do is what
the discussion is all about.

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