Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!ub!uhura.cc.rochester.edu!rochester!kodak!islsun!cok
From: cok@islsun.Kodak.COM (David Cok)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions and other fantasies
Message-ID: <1991Apr19.234958.9400@kodak.kodak.com>
Date: 19 Apr 91 23:49:58 GMT
References: <2202@optima.cs.arizona.edu>
Sender: news@kodak.kodak.com
Organization: Eastman Kodak Co., Rochester, NY
Lines: 24

In article <2202@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>
>So the answer to my original question: "What do you know after a
>formal proof that you did not know before the proof?" is "You know
>that the program implements the formal specification.  You don't
>formally 'know' anything more about the program's real behavior than
>you did before."
>--

You know the same thing after a formal proof that you do after running a test
suite:  if there were errors (failed proof, failed tests) then you have some
bugs to fix; if there were no errors (proof checked, all tests passed) then
you know that the program behavior agrees with (a) the behavior specified by
the specification, or (b) the behavior represented by the test suite.  Both
of the latter are subsets of the full behavior, and neither one necessarily
represents what you really want.  (Yes, I've seen tests that ran into bugs
and no one had properly checked the result of the test.)  If only as a
way of finding more bugs sooner and if only as a way of "verifying" that
an efficiency hack computes the same result as an "obviously correct" but
inefficient alternate program, a program verifier would be useful.

David R. Cok
Eastman Kodak Complany -- Imaging Science Lab
cok@Kodak.COM