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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC 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: kahn@ambra.drcoffsite.com (Larry Kahn) Subject: Re: Problems with proofs Date: 1995/04/21 Message-ID: <4157cb$f21a.59@ambra.drcoffsite.com>#1/1 X-Deja-AN: 101370091 references: <3kaksj$iur@isnews.calpoly.edu> organization: Dynamics Research Corp. reply-to: kahn@drcoffsite.com newsgroups: comp.lang.ada,comp.edu Date: 1995-04-21T00:00:00+00:00 List-Id: In article , cpp@netcom.com says... > ><< [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." > ><< I think you have an idea that a program that is proved correct >is guaranteed to work. >> > hate to jump into this but I agree a proof of correctness is a formal method of proving that the program does what you expect it to do (WITH RESPECT TO A CERTAIN SPECIFICATION)!!!! this is the key... it is only correct with respect to the spec. and if your spec is in error of course the program will not perform correctly. The bottom line is that correctness is a relative term .. I may thing a program should print out a certain error message when certain conditions occur and this was not in the original spec and therefore the developers did not implement it. In terms of the developers the program may still be correct and even verifiable proved as correct with response to a certain spec ... but in my eyes I may say it is incorrect.. this the relativity of correctness (ie relative to individial opinion) But proof of correctness is a formal methodology for proving the program corresponds to what you expect it to do in relation to a specification and this is a different issue than whether or not I believe the program is correct in my eyes... You need to get a book on proof of correctness and look at the definitions more carefully proof of correctness does not proof that the program handles all possible values, never crashes, halts, etc..... I think this is what you are confusing with the term "correctness"..... -- Laurence G. Kahn Senior Software Engineer Dynamics Research Corp. (Finger .site@ambra.drcoffsite.com for PGP public key.) (Internet Phone address: LGK in private forum drcoffsite)