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,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public From: Stuart Palin Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: <5qkun1$35r@gcsin3.geccs.gecm.com>#1/1 X-Deja-AN: 257405210 References: <33CBBF4B.7BAF@pseserv3.fw.hac.com> <33CC64CE.44A3@flash.net> <5qklt1$4el$2@miranda.gmrc.gecm.com> Organization: GEC Marconi Avionics (Rochester) Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: paul.johnson@gecm.com (Paul Johnson) wrote: >The thing is that in Eiffel the assertions are not just a run-time error >detection mechanism, they are also a documentation and specification >mechanism. The Ada assertion was invisible because it was buried in the >implementation of the routine that failed. An equivalent Eiffel routine >(if it were correct) would have had the assertion in its interface, and >so on up to the top level of the software package under discussion. So >anyone reusing the package would have seen the assertion. The Inquiry >specifically commented that the Ada assertion was buried so deeply that >it was effectively invisible to any review. I am not at all convinced by this Paul, in our experiences with SPARK, where formal specifications are hoisted up through the program structure revealing dependencies of lower level routines it is all too easy to end up with an unmanageable number of annotations (assertions). This means that trying to find a possible risk like the Ariane remains impractical using this technique since it is like looking for the proverbial needle in a haystack. This sort of problem would seem to be exacerbated if everyone is creating assertions for every possible thing that could go wrong. -- Stuart Palin Consultant Engineer Flight Systems Division (Rochester) GEC Marconi Avionics Ltd [usual disclaimers to protect the company]