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: fac41,f66d11aeda114c52 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,f66d11aeda114c52 X-Google-Attributes: gid103376,public From: dewar@merv.cs.nyu.edu (Robert Dewar) Subject: Re: Critique of Ariane 5 paper (finally!) Date: 1997/08/21 Message-ID: #1/1 X-Deja-AN: 265780146 References: <33E503B3.3278@flash.net> <33E8FC54.41C67EA6@eiffel.com> <33E9B217.39DA@flash.net> <33EA5592.5855@flash.net> <33EB4935.167EB0E7@eiffel.com> <33EB754E.446B9B3D@eiffel.com> <33EBE46D.2149@flash.net> <33EF9487.41C67EA6@eiffel.com> <33F22B91.167EB0E7@eiffel.com> <33F7C3C0.446B9B3D@eiffel.com> <33FA748A.35FE@flash.net> <33FBD62C.3DD3@invest.amp.com.au> Organization: New York University Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-08-21T00:00:00+00:00 List-Id: Thomas said <> Sure I think we all accept your definition of reliability (the ability of a system to execute correctly ....) although we might want to add something about ease of modification and maintenance (for me these are also aspects of reliability). But that definition is not one we can use directly to ensure reliability. Sure we can judge in retrospect whether we succeeded in generating a realiable application, but we can't use this criterion directly to ensure reliability in advance. If you look at my earlier postings, you will see that the point you are making is *precisely* the one that I emaphasized in my replies to Bertrand. Now what Bertrand claims is that any methodology which results in reliable programs MUST ALWAYS use an approach that includes an explicit use of DBC. What I am saying is that there are many methods and techniques that we use in practice for judging reliability. Correctness is a different property from reliability as you point out (there are unreliable correct programs, and reliable incorrect programs). However, that does not mean that demonstration of correctness is not a useful tool in the quest after reliability. The effort to demonstrate correctness may well show up flaws that would indeed effect reliability. Of course even if you prove total correctness, you have not demonstrated reliability, but then that is true of other techniques (such as formal testing, etc). In practide, we ensure reliability by using a variety of techniques and tools. DBC in the sense in which Bertrand means it is a possible tool. It is neither necessary nor sufficient, but it is one more useful tool (I cannot imagine anyone contesting this point). However, use of DBC does not ensure reliability, and failure to use it does not guarantee unreliability!