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: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/16 Message-ID: <33CD6207.6007@flash.net>#1/1 X-Deja-AN: 257309232 References: <5qi26c$8ll$2@miranda.gmrc.gecm.com> Organization: Flashnet Communications, http://www.flash.net Reply-To: kennieg@flash.net Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-16T00:00:00+00:00 List-Id: Paul Johnson wrote: > > In article , > jsa@alexandria.organon.com says... > > > type Require is boolean range True..True; > >... > > > > Assert : Require := Complex_Precondition(X); > > Interesting idea. However it does not match Eiffel assertions. > > 1: Eiffel assertions are only executed at certain times, not at every > invocation of a routine (see E:TL or OOSC2 for the gory details). OK, so Eiffel's different. What's the significant advantage of this approach. > > 2: You can't inherit assertions. Any such system would require lots > of duplicated assertions. Why would I have to duplicate assertions? > > 3: Invariants are still very tricky to support. You need to call the > invariant checks at the same time as the pre and post conditions. See > above for details of when this occurs. Again, I'm not trying to duplicate Eiffel. How much do I lose if Ada invariants are different? > > 4: You had better be pretty sure that the compiler is not going to > optimise your checks into oblivion during debugging, and conversely > you need a way to turn them off for production code. Actually, I don't mind the checks being "optimized into oblivion" if the compiler can deduce that they are unnecessary, and I certainly don't want to exercise one kind of code during development and another during test. The alternative (as was proposed by one Eiffel advocate) is to not use _any_ assertions for hard real-time threads. If Eiffel compilers do no optimizations of assertions, and there are a lot of complex assertions in Eiffel code, what does this say for the efficiency of the code? > 5: Whilst you could extract the short and flat forms for an Ada class > (sorry, "tagged type"), you can only do so by extending the language > beyond the standard (new special types "require", "ensure", "invariant") > and introducing special coding standards. This kind of non-standard > language extension is one of the things Ada was designed to avoid. Why would you want to _extract_ such information? The contract is in the Ada specification in all of my code, at the level of detail I want public. > > Paul. > > -- > Paul Johnson | GEC-Marconi Ltd is not responsible for my opinions. | > +44 1245 242244 +-----------+-----------------------------------------+ > Work: | You are lost in a twisty maze of little > Home: | standards, all different.