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: 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 From: jsa@alexandria.organon.com (Jon S Anthony) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/13 Message-ID: #1/1 X-Deja-AN: 256682830 Distribution: world References: <01bc8d8c$e608b740$6bb32399@default> <33C5B971.7845@erols.com> <33C831CE.4E56@flash.net> Organization: PSINet Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-13T00:00:00+00:00 List-Id: In article <33C831CE.4E56@flash.net> Ken Garlington writes: > However, compare and contrast: > > (ada-ish): type Foo_Type is range 1 .. 10; > procedure Do_Something ( X : in Foo_Type ); > > (Eiffel-ish): procedure Do_Something ( X : in Integer ); > require X > 0 and X < 11; > > Doesn't seem to make a lot of difference to me That's because there basically isn't any. >, although of course I get to reuse Foo_Type in a lot of static > contexts. Right. But then that's what Eiffel class invariants are about... > As to the more elaborate checks: > > procedure Do_Something (X : in Integer); > > X_Error : exception; > -- raised if X does not meet precondition Complex_Precondition; > > is not particularly more difficult to understand than: > > procedure Do_Something (X: in Integer); > require Complex_Precondition(X); The complexity of the pre/post condition is not an issue. You can get basically the same "expressiveness" in Ada with: type Require is boolean range True..True; ... Assert : Require := Complex_Precondition(X); So, the complexity of the condition is irrelevant. What you can't get at this level of expressiveness are general level class invariants. BUT, > The key is to have the external view of these assertions documented, > and to have violations of those assertions cause certain effects in > the system. Ada has done more than an adequate job in this area for > our safety-critical systems. I don't need more of this; I need more > static analysis tools (as the Safety and Security Annex provides the > foundation to support) and more efficient code, since safety > critical embedded systems usually have a lot of requirements that > preclude using the latest and greatest hardware. sounds a _lot_ more apropos and important. /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