Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!cs.utexas.edu!asuvax!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1882@optima.cs.arizona.edu>
Date: 14 Apr 91 21:34:36 GMT
Sender: news@cs.arizona.edu
Lines: 14

In article  <50453@nigel.ee.udel.edu> Darren New writes:
]If by "correct" you mean "meets the specification" then the ability to
]show that the behavior of the program is related to the behavior
]of the specification is a testing-equivalence sense can be very helpful.

Of course that's what "correct" means.  But the "specification" is an
informal description of what the program should do.  A _formal_
specification can be as wrong as a program can.  And in general the
process of writing a formal specification can be a buggy as the
process of writing a program.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman