Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!mips!dimacs.rutgers.edu!rutgers!mcnc!uvaarpa!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: <12APR91.20195376@uc780.umd.edu>
Date: 12 Apr 91 20:19:53 GMT
References: <1755@optima.cs.arizona.edu> <1991Apr11.214018.19443@watmath.waterloo.edu> <11APR91.19210188@uc780.umd.edu> <1991Apr12.125553.7307@watmath.waterloo.edu>
Sender: usenet@ni.umd.edu (USENET News System)
Organization: The University of Maryland University College
Lines: 63
Nntp-Posting-Host: uc780.umd.edu

Michael Coffin >
Me             >|

>|eh?  imperative programming languages don't say "achieve this goal" ?
>No.  Imperative languages specify a series of actions, not the
>results of those actions.

umm.. hmm...

I'm not totally sure I see the difference.

If I have a routine that sorts numbers so that the result is
monotonically increasing, doesn't the closure of that routine with
some numeric list specify the results?

>|...if I say "sort this list" that's [what] 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".

Er.. yes, in that proofs generally are sets of equivalent statements
about the same "data" (often denumerable sets, or what-have-you).  But
even in proofs, you can deal with expressing A in form B.

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).

I'll grant you that an imperative language transforming data is doing
something different than a proof about some form(s) of that data.  But
what about an imperative language transforming some set of statements
to some equivalent set of statements (like a compiler, or a symbolic
math engine)?

I think it's just a matter of what's being transformed.

No??

Well, I guess some proof techniques are O(godawful).  But that's what
people are for...

>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.

Hmm... so what you're talking about is introducing new concepts to a
language or system.  I think that technically this falls into the
category of "meta-proofs" rather than "formal proofs".

Correct me if I'm wrong :-)

I know somebody will...

Raul Rockwell