Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!sdd.hp.com!cs.utexas.edu!rutgers!rochester!kodak!islsun!cok
From: cok@islsun.Kodak.COM (David Cok)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions and other fantasies
Message-ID: <1991Apr21.015422.7522@kodak.kodak.com>
Date: 21 Apr 91 01:54:22 GMT
References: <2216@optima.cs.arizona.edu>
Sender: news@kodak.kodak.com
Organization: Eastman Kodak Co., Rochester, NY
Lines: 54

In article <2216@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
> ...
>
>In article <???> cok@Kodak.COM (David Cok) writes:
>]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.
>
>You have missed the entire point of the article: the behavior
>specified by the specification may bear no relation to the correct
>behavior for the program.  Thus knowing about the formally specified
>behavior does not tell you about the correctness of the behavior.  I'm
>talking about what you _know_ in the sense of mathematical certainty.
>

I didn't miss your point.  You stopped quoting my post too soon:

Both of the latter are subsets of the full behavior, and neither one necessarily
represents what you really want.


I meant -- are at best subsets of the full behavior.
In fact I mostly agree with you: formal proofs do not give certainty because
specs may not match the desired behavior.  However, I still think that a
verifer could (the technology is nowhere near providing this yet) be a
valuable complement to testing (for which we have some useful technology now),
something people might run on programs as they might run lint on a C program.  
It does not give certainty but it can raise confidence.  It only relates two 
formal specs, but if one is simpler and, to the human reader, more clearly 
correct, then there is good reason for some increased confidence.  And if the
verifier points out an error, you are one bug ahead.  The confidence is 
misplaced if the spec is incomplete or inaccurate, but that is 
also true for an incomplete test suite.   


>Formal verification is now and
>always will be a special technique that is only useful in certain
>kinds of applications, and always in conjunction with testing. 

And everything useful was already invented by 1900. :-)

>
>Disclaimer: Nothing in the above should be taken as an assertion that
>program verification has no value.  It is only intended to clarify
>exactly what is (and is not) mathematically proven by a formal proof
>of correctness.

OK.  On those points we agree.

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