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, LOTS_OF_MONEY 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: "Howard W. LUDWIG" Subject: Re: Design by Contract (was Re: Interesting thread in comp.lang.eiffel) Date: 2000/07/12 Message-ID: <396C7F14.563F1BA4@lmco.com>#1/1 X-Deja-AN: 645486458 Content-Transfer-Encoding: 7bit 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> X-Accept-Language: en,pdf Content-Type: text/plain; charset=us-ascii Organization: Lockheed Martin -- Information Systems Center Mime-Version: 1.0 Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-12T00:00:00+00:00 List-Id: David Kristola wrote: > On Tue, 11 Jul 2000 6:14:44 -0700, Ken Garlington wrote > (in message <85Fa5.11419$7%3.818927@news.flash.net>): > > > convert (horizontal_bias: INTEGER): INTEGER is > > require > > horizontal_bias <= Maximum_bias > > I'm not saying that Design by Contract is a bad thing, > but i hope there is a whole lot more to it than this > example seems to say. I saw a similar example for a > formatted comment in Java that can be checked by a > tool. > > Ada does the above by using a subtype that is limited > to Maximum_Bias. (The Java example had a post condition > contract saying that the out parameter would be > positive, again, the Ada solution is to use a subtype). > > What kinds of DbC things could i do in Eiffel that i > can't do in Ada with pragma Assert and good typing? > > How can i use the concepts of DbC to make better Ada > code? > > Thanks, > > -- > --djk, keeper of arcane lore & trivial fluff I would like to add my own questions--actually add some specificity to David's questions. I have never coded in nor learned Eiffel before, so _some_ of these concepts are new to me and I am a bit confused. In particular: 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? The reason I ask is that I have read in this thread and in skimming through OOSC that in a contract, using Eiffel/ DbC principles, a caller is responsible for verifying the preconditions (the "require" block) and the callee is responsible for verifying the postconditions (the "ensure" block). How does the caller handle the verification of the preconditions if they are spelled out in [only] the callee? I'm interested in the overall DbC philosophy on this topic of verifying contracts, the Eiffel implementation, and what and how much can be done similarly in Ada implementations. The DbC distribution of responsibility for satisfying contracts seems to be clean--somewhat different from what is usually done, and I'm not totally convinced yet that it is the best way to go, but _at least_ it is a well-defined way, which is better than having no way and taking a haphazard approach. Range-checking on Ada subtypes seems to take the DbC approach in general, but full-fledged assertions would seem to execute wherever they are written, which imposes most of the burdens, whether pre- or post-conditions on the callee. Any clarification would be most appreciated. Howard W. LUDWIG