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.3 required=5.0 tests=BAYES_00,FROM_ADDR_WS, 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/19 Message-ID: <8l4v6n$3mph1$1@ID-9852.news.cis.dfn.de> X-Deja-AN: 648316441 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> <8kl0r6$2lp6o$1@ID-9852.news.cis.dfn.de> <01HW.B59443DD000A71F808C44DCC@news.pacbell.net> <8kt1eb$34jh1$1@ID-9852.news.cis.dfn.de> <01HW.B59822A20005ECF4078EC70C@news.pacbell.net> X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2314.1300 X-Trace: fu-berlin.de 964034583 3892769 195.190.10.210 (16 [9852]) X-MSMail-Priority: Normal Reply-To: "Joachim Durchholz" Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-19T00:00:00+00:00 List-Id: David Kristola wrote: > On Sun, 16 Jul 2000 12:12:10 -0700, Joachim Durchholz wrote > (in message <8kt1eb$34jh1$1@ID-9852.news.cis.dfn.de>): > > > David Kristola wrote: > >> On Thu, 13 Jul 2000 11:12:53 -0700, Joachim Durchholz wrote: > >> > >>> or > >>> find_minimum_in (h: HEAP) > >>> require > >>> not h.is_empty > >> > >> Depending on the implementation of the heap, this too would > >> probably cause some sort of exception to be raised if the > >> heap were empty. > > > > The difference is that the exception will happen before the routine > > is even called. The responsibility for the exception will clearly > > be the caller's. > > If the exception happens somewhere inside the routine, you need > > another analysis step to find out which part of the code is really > > responsible for the problem. > > Perhaps it is my coding style, but (in this limited case) i would > consider it the responsibility of the caller to handle the exception. Oh, this is not a limited case. The vast majority of failed assertions is in precondition checks (well, at least during debugging.) In nearly all cases, the caller needs to be fixed. (There is the rare occurrence that a precondition was needlessly strict. If we own the library with the callee, we take the opportunity to weaken the precondition in this situation.) > There is nothing find_minimum_in can do if the heap is empty. To me, > that is even an unstated but obvious contract. The difference is that the contract is explicit. Besides, the contract isn't obvious. The routine could reasonably return some minimum value if the heap is empty. In that case, we'd have one precondition less and one postcondition more. > This is not to say > that it is not worth stating obviously and in a way that can be > checked by a compiler. This particular example is perhaps a little > simple. Certainly there are plenty of others that are not so > obvious, where a formally stated precondition adds to the understanding. It's usually the other way round: Writing preconditions can relieve you of verbiage in the description. Say you have a routine like this in FILE: read (offset, number_of_bytes: INTEGER; target: BUFFER) -- Read 'number_of_bytes' bytes into 'target', starting at file -- offset 'offset'. -- File must be open. -- Do not try to read past end-of-file. This can be rewritten in a more concise and formal way as read (offset, number_of_bytes: INTEGER; target: BUFFER) -- Read 'number_of_bytes' bytes into 'target', starting at file -- offset 'offset'. require must_be_open: open dont_read_past_eof: offset + number_of_bytes <= file_size + 1 where 'open' and 'file_size' are other functions of FILE. The first interface is what you usually read in some software description. It leaves much to desire: there is no indication what will happen if the preconditions aren't fulfilled, and it doesn't tell the programmer what exactly has to be done to make sure that the call will not fail. The second interface is clearer. The reaction to a failed precondition will always be an exception, or unspecified behaviour if checking is switched off. This is quite harsh, but people tend to write short preconditions; if clients of 'read' want a less strict contract (say, reading past EOF fills the rest of 'buffer' with null bytes or whatever) then bugger the routine author. It's also *much* more precise: the preconditions leave no question open. The caller must make sure that the 'open' query on the FILE returns True, and he must fulfill some precisely defined numeric inequation on 'offset' and 'number_of_bytes'. The caller can then republish the same contract on its own interface (if the caller has such a things as 'offset' and 'number_of_bytes'), or it can translate the preconditions to some higher abstraction. For example, a class that embodies a file with fixed-length records might have this routine: read (record_number: INTEGER; target: FIXED_LENGTH_RECORD) require must_be_open: open dont_read_past_eof: record_number <= number_of_records do internal_file.read (record_number * record_size, target.size, target) end open: BOOLEAN do Result := internal_file.open end number_of_records require must_be_open: open do Result := internal_file.number_of_bytes div record_size end I'm leaving out details like checking that the file size is an integral multiple of record_size, a check that will probably be done in the 'open' routine; to ensure that this is always true, we can write this: invariant integral_records: internal_file.number_of_bytes mod record_size = 0 Together, these specifications make sure that FILE's 'read' routine will never be called with inappropriate parameters. Well, unless I overlooked something - it's a bit late right now and I don't have the time to check that the preconditions percolated up precisely. In a real-life situation, I'd make sure that this really holds up, either by extensive testing, or by code review; in an ideal world, I'd ask an inference engine whether the 'read' call guarantees all its preconditions. > Ada also does not provide for the inheritance of contracts. That is > a very interesting aspect of Eiffel. Actually this is the main concept in Design by Contract. It's essentially the Liskov Substitutability Principle applied to preconditions and postconditions: If you have a variable of type PARENT, and assign to it an object of type CHILD, then everything should work as expected - in other words, all routines in CHILD must honor all contracts that the precursor routines in PARENT offered. (CHILD may offer more value: its routines may require less of the caller, i.e. loosen up the precondition, or they may guarantee more, i.e. specify a stricter postcondition.) Regards, Joachim -- This is not an official statement from my employer or from NICE. Reply-to address changed to discourage unsolicited advertisements.