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: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/23 Message-ID: <33FFAAB0.714@flash.net>#1/1 X-Deja-AN: 268276644 References: <33E09CD5.634F@flash.net> <33E9ADE9.4709@flash.net> <5siqrr$3of@jupiter.milkyway.org> <5smgts$p68$1@miranda.gmrc.gecm.com> <33EFCCE4.4CE0@flash.net> <5sskfd$nn5$2@miranda.gmrc.gecm.com> <33F25AA5.49ED@flash.net> <5t1fen$c7d$1@miranda.gmrc.gecm.com> <33F52989.38BB@flash.net> <33F83585.2FB006C3@munich.netsurf.de> <33FA76D7.21D9@flash.net> <33FAB35A.18AA15BB@calfp.co.uk> <33FD55E3.CE8A29BF@calfp.co.uk> Organization: Flashnet Communications, http://www.flash.net Reply-To: Ken.Garlington@computer.org Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-23T00:00:00+00:00 List-Id: Nick Leaton wrote: > > OK, so if you can't write such requirements in a rigorous way, how can > you write the application. If you can write an application that meets > the requirements, you can write a coded spec for the problem. In the > extreme case, the code for the application is the specification. Welcome to the Ariane IV problem! The code is an _implementation_ of the specification. Except for trivial cases, it is not the _only_ implementation. Furthermore, the specification can state things not related to the implementation -- in particular, the assumptions of the physical environment -- at a level that can be (a) subjective and (b) non-implementable as code. The code still works, since it doesn't have to encode such assumptions. > If you > cannot code the spec/requirements you can't check that they work. Just > because you have a deficient spec, or because you cannot envision what a > set of DBC assertions are for a problem doesn't detract from DBC. Being able to implement a spec, and being able to test the implementation, is not the same as saying that the code can replace the spec. This is a lesson learned from Ariane. For more information, read my paper (or the inquiry report, referenced from that paper). > > -- > > Nick