Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!brutus.cs.uiuc.edu!uakari.primate.wisc.edu!uflorida!mephisto!mcnc!duke!romeo!crm
From: crm@romeo.cs.duke.edu (Charlie Martin)
Newsgroups: comp.software-eng
Subject: Re: What's Right and Wrong About Charles Martin's Position
Keywords: correctness, validation, testing, program verification
Message-ID: <17811@duke.cs.duke.edu>
Date: 26 Feb 90 17:07:12 GMT
References: <3237@umn-d-ub.D.UMN.EDU>
Sender: news@duke.cs.duke.edu
Reply-To: crm@romeo.UUCP (Charlie Martin)
Organization: Duke University CS Dept.; Durham, NC
Lines: 74


In response to at least one question, the reason I continue arguing with
Dr Fetzer is  (1) I've got more dedication to the old business about the
pursuit of truth than I do sense, and (2) I really do think the issues
are important and significant.

Now, I'd like to summarize my position briefly (believe it or not):

(1) I recognize the distinction Dr Fetzer makes between deductive
    knowledge and scientific or inductive knowledge.  He was right about
    the distinction, as I've said all along.  However, it was not a new
    idea in the community or a new distinction.

(2) Hoare has said in print that once a program is proven tests are no
    longer needed.  (See e.g. pg 319 of Hoare and Jones _Essays in
    Computing Science_, in the paper "Programming is an Engineering
    Profession".)  I believe this is folly.

(3) However, I do not believe that Dr Fetzer's paper and its publication
    represented good or responsible scholarship, for the following
    reasons:

    (a) It presented no new information.  The issue he drew was one that
    is well-known in the literature.  It makes no mention of other
    considerations of the same problem is widely-accessible
    publications.  (examples follow.)

    (b) After several re-readings, it still appears to me to state that
    program verification per se is fatally flawed, not just Hoare's
    position with reference to testing.  My previous posting notes
    several reasons why I believe it gives that impression.

I promised examples.  Here are two, drawn from the books I can reach
with my left hand from my desk.

From "Mechanical proofs about computer programs", Donald I Good, in
Hoare and Shepherdson _Mathematical Logic and Programming Languages_, pp
70-71. (Prentice-Hall, 1985)

   "However, there are several reasons why a program that has been
    proved within the Gypsy environment may not behave exactly as
    expected.  First, the formal specifications may not describe exactly
    the expected behavior of the program.  Secondly, the formal
    specification may not describe all of the aspects of program
    behavior.  Thirdly, invalid lemmas may have been assumed without
    proof. Finally, either the verification environment, the compiler,
    the Gypsy run-time support or the hardware might malfunction.

    ....These sources of error are cited not to belittle the potential
    of a scientific basis for software engineering but to make clear
    that the formal, mathematical approach offers no absolutes."

From _Formal Methods of Program Verification and Specification_, Berg et
al., pg 36.  (Prentice-Hall 1982)

   "Another limitation arises from the necessarily abstract view we take
    of program semantics and the corresponding distance that exists
    between a formally verified program and the physical manifestation
    of its behavior. .... The functioning of the hardware is a physial
    process, subject to the laws of nature.  Ultimately, then, the
    confidence we have in the correctness of a program depends upon our
    belief that the proper physical actions will result.  As a result,
    there is no "bottom line" at which we can show that executing a
    program is guaranteed to produce the desired effect.  The best we
    can do is show that programs are correct with respect to their
    execution on some abstract machine, which we model with a deductive
    system.  The _truth_, as opposed to the validity, of the theorems in
    the deductive system depends upon the proper implementation of the
    program semantics--that is, of the abstract machine--by hardware and
    software."

I believe these two quotes show that Dr Fetzer's position was well-
understood and widely recognized long before his paper was published.
Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)