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: 103376,59dddae4a1f01e1a X-Google-Attributes: gid103376,public From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: Software Safety (was: Need help with PowerPC/Ada and realtime tasking) Date: 1996/06/08 Message-ID: #1/1 X-Deja-AN: 159184711 references: <31AD794D.2E62@lmtas.lmco.com> <4p4trk$tc5@watnews1.watson.ibm.com> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.ada Date: 1996-06-08T00:00:00+00:00 List-Id: "I agree. About a decade ago, at workshop on formal verification of Ada programs, I got into a heated argument with David Gries about a useful definition of correctness. I argued that it was useless to prove a program conformant to formal specifications unless one had a high degree of confidence that the specifications expressed the customer's intent. Gries seemed to have in mind a model whereby the customer presents the software developer with a contract expressed in the form of formal specifications; if the software developer conforms to the specifications, he has fulfilled the contract, even if the customer doesn't get what he really wanted. " I certainly agree that it is unfortunate that the term correct has been hijacked, however, it is tilting at windmills to try to change this now (sort of like my efforts to prevent the misuse of moot and oxymoron :-) Your "heated argument" reminds me of a conference I was at where Niklaus Wirth was talking about programming being a process of refinement whre the one and only issue was that refinement should be correctness preserving. At the end of the panel session, I commented that the whole notion of correctness is misguided, because the issue is building reliable software, not correct software. I used as an anology car manufacture, car companies are interested in building reliable cars, almost no one would talk about a correct car. And indeed almost any car does NOT meet its specifications, but the issue is whether the defect are minor. A small area of miscolered paint under the rear bumper renders a car incorrect, but not unreliable! In the case of softare, correct and reliable are of course NOT the same. Reliability includes the specificatoin being correct, and of course we have no way of proving a specification correct, at most we could prove it consistent, but that might simply mean it is consistently wrong! Actually as specifications get more formal, it often gets harder and harder to determine if it is correct. Try looking at the formal definition done by the EEC for Ada 83, it is two fat telephone books of mathematical formula -- and there is no way of ensuring it is correct [in fact, as would be expected for what is essentially a huge program that has never been run, it is not correct]. On the other hand, a program that trivially departs from its spec (background of the GUI is slightly different shade of green than specified for example) may still be completely reliable even though it is not correct. So I prefer to leave the term correctness to (mis)mean what David Gries and Niklaus Wirth (and many others) insist on, and simply to recognize that it is not the most important property, and if I am a customer I want a program that works, a correct (in this sense) program that does not work is of no interest to me, and I will not sign a contract that says that all the program has to do is to implement correctly some formal specification! P.S. At that panel session, when I made the comment about cars not having to be correct, the audience, quite frustrated I think with the panel presentation, applauded the comment loudly :-)