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,e01bd86884246855 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,fb1663c3ca80b502 X-Google-Attributes: gid103376,public From: "Eirik Mangseth" Subject: Re: Design by Contract (was Re: Interesting thread in comp.lang.eiffel) Date: 2000/07/12 Message-ID: #1/1 X-Deja-AN: 645569718 References: <8ipvnj$inc$1@wanadoo.fr> <8j67p8$afd$1@nnrp1.deja.com> <395886DA.CCE008D2@deepthought.com.au> <3958B07B.18A5BB8C@acm.com> <395A0ECA.940560D1@acm.com> <8jd4bb$na7$1@toralf.uib.no> <8jfabb$1d8$1@nnrp1.deja.com> <8jhq0m$30u5$1@toralf.uib.no> <8jt4j7$19hpk$1@ID-9852.news.cis.dfn.de> <3963CDDE.3E8FB644@earthlink.net> <3963DEBF.79C40BF1@eiffel.com> <396502D2.BD8A42E7@earthlink.net> <39654639.B3760EF2@eiffel.com> <85Fa5.11419$7%3.818927@news.flash.net> <01HW.B591811303737A0605DE478C@news.pacbell.net> <396C7F14.563F1BA4@lmco.com> <07634490.b099171e@usw-ex0107-055.remarq.com> X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2919.6600 X-Complaints-To: news-abuse@online.no X-Trace: news1.online.no 963425368 130.67.73.101 (Wed, 12 Jul 2000 20:09:28 MET DST) Organization: Telenor Online Public Access X-MSMail-Priority: Normal NNTP-Posting-Date: Wed, 12 Jul 2000 20:09:28 MET DST Newsgroups: comp.lang.eiffel,comp.lang.ada Date: 2000-07-12T00:00:00+00:00 List-Id: "Greg" wrote in message news:07634490.b099171e@usw-ex0107-055.remarq.com... > "Howard W. LUDWIG" wrote: > [snip] > > > >How are the "require" and "ensure" blocks handled--as > >executable code at run-time, as compiler-checking, or > >simply as comments to support humanoid review or automated > >checking by tools other than the Eiffel compiler? Assertion checking is done at run-time, with the strictness-level set by the programmer. In addition Eiffel IDE's come with tools like short and flat/short. The first produces a public view of the class, i.e. all exported features including pre- and postcondtions and the class invariant (if present). The latter (flat/short) produces the same format, but includes features and assertions from all ancestors of the current class. This makes for very compact and readily available documentation which, in the Eiffel IDE I'm using can be output in various formats, including html (with hyperlinks an all), tex, troff, etc. It is also possible to write your own pluggable "filters". Someone in this thread commented that a weakness was that assertions are scattered throughout the code and that it would be better to have them in a separate file. First of all, an assertion is intimately linked to the feature it applies to. If it is a so-called business rule it should be declared in only one place, i.e. the class that defines the abstraction to which the rule applies. That way, it is not "scattered" throughout. Secondly, there's no need to keep assertions in a separate file e.g. for documentation purposes as the above mentioned tools will produce the necessary documentation (also from the command line). > > AFAIK no Eiffel compiler can check require/ensure code at run- > time. A typo here, Greg? Should say compile-time, shouldn't it? Regards Eirik Mangseth Stockpoint Nordic AS, Lysaker, Norway "If I can't Eiffel in heaven, I won't go" > Indeed, many of the assertions simply can't be computed > until runtime. > > Compiler options can be used to toggle sets of assertions. ISE's > ACE (their makefile language) takes this control down to the > class level. So developers have a degree of control over how > much overhead the assertions add. > > The burden of executing 'require' clauses need not be placed on > the callee. In examining the interface to a class, the compiler > has all the information needed to place that burden in the > caller's code. It simply inline's the require clauses before the > feature call. This is one reason that any features referenced by > a require clause have to be public. > > For example, in the STRING class the index method (in > SmallEiffel) is declared as: > > item (index: INTEGER): CHARACTER > -- Character at position index. > require > valid_index(index) > > Here valid_index is a public feature. When a client of string > executes: > c := str.item (n) > the compiler may translate this into (pseudo-C code): > assert (str.valid_index(n)) // inlined require clause > c := str.item (n) // actual execution > > So in principle one can deliver an Eiffel library as interface > definitions and optimized code, and still get the benefits of > DbC. > > (Ensure clauses are a different matter. They can access private > data and have to be compiled into the service object. Ideally, > if one ships an optimized binary library, one's already done a > lot of work to make sure that all the ensure clauses are > redundant.) > > The require/ensure clauses are also a great humanoid review tool. > See for example the ongoing ELKS 2000 standardization process, > http://www.egroups.com/group/eiffel-nice-library > Practically all of the discussion focuses on feature names and > the require/ensure clauses supported by the features. Rarely are > implementation details discussed, and comments are used > sparingly. (Try THAT in C++ why doncha!) > > [snip] > > > > ----------------------------------------------------------- > > Got questions? Get answers over the phone at Keen.com. > Up to 100 minutes free! > http://www.keen.com >