From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 10db24,77f71d0bde4c5bb4 X-Google-Attributes: gid10db24,public X-Google-Thread: 103376,86fd56abf3579c34 X-Google-Attributes: gid103376,public From: cpp@netcom.com (Robin Rowe) Subject: Re: Problems with proofs Date: 1995/04/20 Message-ID: #1/1 X-Deja-AN: 101283289 sender: cpp@netcom6.netcom.com references: <3kaksj$iur@isnews.calpoly.edu> organization: NETCOM On-line Communication Services (408 261-4700 guest) newsgroups: comp.lang.ada,comp.edu Date: 1995-04-20T00:00:00+00:00 List-Id: To: dewar@cs.nyu.edu (Robert Dewar) Robert, I mistakenly attributed your post to Steve Tate, and replied to him. Here's the reply I intended to your post. << Nope [to that proofs are based on what appears relevant to a human being to prove], proofs are based on formal specifications of the task at hand. >> So, it's not human beings who decide what belongs in the formal specifications? By the way, please define the term "formal" as you are using it here with regard to specifications. << This [that there is no proof that the proof is equivalent to the code] is based on a misconception, a proof of correctness, if is is any use at all, must have a formal relationship to the code. >> Please define the term "formal" as you are using it here. << Typically assertions in the code are used to guide an actual proof of the correctness of the actual code. Nothing else is useful. >> I'm not clear what you are trying to say here. Are you really saying that the only really useful proofs are those expressed in code? (I think so, too, but this is a radical viewpoint.) << Proofs of correctness must be machine verified to be accepted. >> Please define the term "verified" as you are using it here. << Interfaces to components are part of the axiomatic structure of proven components, and on one side you prove that a component properly handles uses that conform to its interface, and on the other, you prove that the use by a client conforms to this interface. >> This sounds reasonable, and what I expected, too. However, I've been told that valid ranges are often specified arbitrarily. Invalid input is the user's (engineer's) lookout. Have I been misinformed? Is it generally more comprehensive? << I have no idea what you mean by random error. >> Cosmic rays, accidents, etc. << [Proofs take into account hardware failure] if the spec includes this, and they don't if the spec does not. >> Isn't this a pretty loose way to look at proof? Proving that you conformed to a (possibly erroneous) specification sounds a lot less impressive than saying you have a "proof of correctness." In fact, the term seems very misleading since I don't think it is really proven in the mathematical sense nor correct in the engineering sense. << I think you have an idea that a program that is proved correct is guaranteed to work. >> A mind reader you're not. << If you have a 100% track record in implementing code that exactly conforms to its specifications, wonderful! I think proof of correctness won't help, but if, like most people, you find that one of the many weak links on the chain is in incorrect implementation of specifications, then proof of correctness....>> Hmmm, I may have to change my mind about the utility of the halting problem. Implementing code that exactly conforms to its specifications sounds like the halting problem to me. Thanks for the feedback. Good points. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter!