Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!bellcore!decvax!decwrl!glacier!kestrel!ladkin
From: ladkin@kestrel.ARPA (Peter Ladkin)
Newsgroups: net.cse
Subject: correctness
Message-ID: <6042@kestrel.ARPA>
Date: Thu, 20-Mar-86 22:16:33 EST
Article-I.D.: kestrel.6042
Posted: Thu Mar 20 22:16:33 1986
Date-Received: Sat, 22-Mar-86 23:40:05 EST
Organization: Kestrel Institute, Palo Alto, CA
Lines: 22

Some comments have recently been made in this group to the 
effect that it's not feasible to *prove* correctness of a
term project program.
Prima facie, this is false. If the program is specified in
terms of its exact output on a small finite number of test
cases, then the program may be *proved* correct by exhaustive
testing. It is indeed the case that an assumption has to be
made about the environment (e.g. the Pascal compiler does
not generate code that will side-effect any processes other
than I/O and memory management,......) but it is standard
to make this assumption for serial processes.
Of course, this might not be an *interesting* program
specification in many cases, but it does have pedagogical
value.
One usually wants to make some extra conditions on the 
program, such as, it must be generalisable (which in this
case would ensure that the program didn't just case-test-
and-print). But this is not a question of correctness
from this specification. It would be in others (*parse
all Pascal programs...*)

Peter Ladkin