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.6 required=5.0 tests=BAYES_20,INVALID_MSGID 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: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public From: Ian Rae Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/18 Message-ID: <33CFA084.3DA1@nt.com>#1/1 X-Deja-AN: 257596408 References: <33CBBF4B.7BAF@pseserv3.fw.hac.com> <33CC64CE.44A3@flash.net> <5qklt1$4el$2@miranda.gmrc.gecm.com> <5qkun1$35r@gcsin3.geccs.gecm.com> Organization: IDEAS CTI, Nortel Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-18T00:00:00+00:00 List-Id: Stuart Palin wrote: > > 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. Good point; assertions tend to be used for both interface and implementation assumptions. However, assertions have the nice property of playing two roles: (a) as documentation in the source code, and (b) as run-time checks. The needle that can't be seen will be identified when it jams up the baler machine. This, of course, assumes you're making very small bales (ie. doing very rigorous testing). --Ian Rae Senior Systems Developer Nortel IDEAS CTI Group