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/20 Message-ID: #1/1 X-Deja-AN: 265512629 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> Organization: New York University Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-08-20T00:00:00+00:00 List-Id: Bertrand said <<> The definition of reliability which this implies is that a system > is "highly reliable" if it has been working satisfactorily for, > say, 30 {seconds | minutes | hours | days | weeks | months | years} > -- pick one. This is one possible definition of reliability, which gets > more and more interesting as it moves to the right of the list > of choices; but it is by no means the only "terms that matter".>> Incidentally I said nothing of the kind in my message, I said that the only measure of reliability that made any sense was that a program behaved in a realiable manner and did what it was supposed to do. The idea that this implies that I think the only possible test of this is to run the system and see if it works is an idea created by the reader not the writer! There are many ways that one can use to determine if a program is reliable. For example, in some limited small cases, total proof of correctness may be a useful tool. Certainly the contstruction of such proofs can be aided by accurate assertions about the code, but such proofs do not (and cannot) depend critically on the presence of such assertions. Similarly, systematic coverage and branch testing are pretty much independent of whether DBC was or was not used. Showing that a program is realiable is a complex process that involves the use of many tools and techniques. Yes, in some cases, DBC may aid this process, but the suggestion that no program can be realiable which does not use DBC is plain unreasonable.