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: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public From: jsa@alexandria.organon.com (Jon S Anthony) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: #1/1 X-Deja-AN: 257539687 Distribution: world References: <5qi26c$8ll$2@miranda.gmrc.gecm.com> Organization: PSINet Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: In article <5qi26c$8ll$2@miranda.gmrc.gecm.com> paul.johnson@gecm.com (Paul Johnson) writes: > 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. Never said it did. I simply said that the complexity of the condition does not prevent a similar expression in Ada to that in Eiffel. That still stands. > 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). Yeah, I've looked at this - what's the point?? > 2: You can't inherit assertions. Any such system would require lots > of duplicated assertions. Sigh, for the _umpteenth_ time: Yes you can! The correct statement here is that you don't have _general_ class invariants without "programming" them. But constraints _are_ inherited. And besides, why is just waving "inheritance" around supposed to mean something "important"??!?!? Believe me - from my perspective it has _long_ since lost any magical luster it may have once had in SWE. > 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. This is just point 2 repeated... > 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. ??? As long as it is _legal_ (does not change the _meaning_ of the code) this would be a _good_ thing! It amounts to verification at _compile_ time. > 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. Who cares about the bogus short flat form? That is simply an error prone method for describing interfaces. Ada has no need for it as it makes this stuff explicit! /Jon -- Jon Anthony OMI, Belmont, MA 02178 617.484.3383 "Nightmares - Ha! The way my life's been going lately, Who'd notice?" -- Londo Mollari