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,FROM_ADDR_WS, 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,e01bd86884246855 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,fb1663c3ca80b502 X-Google-Attributes: gid103376,public From: "Joachim Durchholz" Subject: Re: Design by Contract (was Re: Interesting thread in comp.lang.eiffel) Date: 2000/07/13 Message-ID: <8kl0r6$2lp6o$1@ID-9852.news.cis.dfn.de>#1/1 X-Deja-AN: 645999033 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> X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2314.1300 X-Trace: fu-berlin.de 963511974 2811096 195.190.10.210 (16 [9852]) X-MSMail-Priority: Normal Reply-To: "Joachim Durchholz" Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-13T00:00:00+00:00 List-Id: Howard W. LUDWIG wrote: > David Kristola wrote: > > > What kinds of DbC things could i do in Eiffel that i > > can't do in Ada with pragma Assert and good typing? Stuff like my_parame /= Void or find_minimum_in (h: HEAP) require not h.is_empty or solve (q: QUADRATIC_EQUATION) require solvable (q) or sqrt (r: REAL): REAL is require r >= 0.0 or log (r: REAL): REAL is require r > 0.0 (try to put both the preconditions for sqrt and log into a range type ). It's just more flexible. In fact Eiffel has no range types; the understanding is that contracts properly include them. (Personally, I tend to disagree but I can live well with just contracts.) > How are the "require" and "ensure" blocks handled--as > executable code at run-time, Usually, provided that you have switched run-time checking on (e.g. because you're testing your code - it's not usually done in production code). > as compiler-checking, In principle, yes. No such tool has yet been built though; it would require a) a quite powerful inference engine and b) some way to allow programmers to help with inferences if the engine doesn't come up with a proof, or c) meaningful warnings that pinpoint the problem so that the appliation programmer either knows what to change in his code or can prove validity by hand. It would be an interesting large project to do that. Most inference engines are built for academic languages. > or > simply as comments to support humanoid review or automated > checking by tools other than the Eiffel compiler? This usage is always a part of DbC. It tends to be more important than the checking aspects. > How does the caller handle the > verification of the preconditions if they are spelled > out in [only] the callee? As David wrote, it's usually done by the compiler which compiles everything in one large blob (no separately compiled libraries). But that's just an accident of current Eiffel implementations. For example, for sqrt (r: REAL): REAL is require r >= 0.0 an Eiffel compiler could emit assembly code like this: _checked_sqrt: = 0.0" sqrt: _start_sqrt: That way, it's the caller's choice: if it calls _checked_sqrt, it's getting the precondition checking, if it calls sqrt, it's getting no precondition checking. The code for raising an exception in the caller should just unwind the stack and raise the exception, while the code for raising a postcondition exception does not unwind the stack. (The exact details of exceptions depend on the presence of debuggers etc., so I won't go into detail here.) > 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. I have used DbC in practice, and it is immensely useful. I used to write "defensive code" in the past, and always had the problem that I never knew what my code should do if it really detected a problem. Then I had the same checking in the callers... and lots of trouble whenever the specifications of the code changed. Today, I do the same defensive programming and put it into the preconditions. However, I don't code them in the caller anymore (so the caller doesn't have to worry whether he really understood the documentation - the callee should do all the relevant checks), the caller doesn't have to worry about the inefficiencies of defensive programming (just switch assertions off for the code that you're confident in). Regards, Joachim -- This is not an official statement from my employer or from NICE. Reply-to address changed to discourage unsolicited advertisements.