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.1 required=5.0 tests=BAYES_00, PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,d3770aac68211766 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Received: by 10.180.101.2 with SMTP id fc2mr197100wib.0.1353056025239; Fri, 16 Nov 2012 00:53:45 -0800 (PST) MIME-Version: 1.0 Path: ha8ni292754wib.1!nntp.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!94.232.116.13.MISMATCH!feed.xsnews.nl!border-3.ams.xsnews.nl!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!novia!news-hub.siol.net!news1.t-com.hr!newsfeed.CARNet.hr!feeder.erje.net!eu.feeder.erje.net!newsfeed.straub-nv.de!nuzba.szn.dk!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Class wide preconditions: error in the Ada 2012 Rationale? Date: Thu, 8 Nov 2012 18:57:51 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1352422674 21470 69.95.181.76 (9 Nov 2012 00:57:54 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 9 Nov 2012 00:57:54 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-RFC2646: Format=Flowed; Response Date: 2012-11-08T18:57:51-06:00 List-Id: "Yannick Duch�ne (Hibou57)" wrote in message news:op.wnbifyvyule2fv@cardamome... >I have a doubt, and this one disturb me, so this topic. > ... >> In summary, class wide preconditions are checked at the point of call. >> Class wide postconditions and both specific pre- and postconditionsare >> checked in the actual body. > >I believe either my understanding is wrong, or the Rationale is wrong. The above is correct. > The above statements are not compatible with the substitution principle. *Specific* preconditions and postconditions are not necessarily compatible with the substitution principle. If you want that, you either have to be careful what you write, or (better IMHO) use only class-wide preconditions and postconditions. You don't always want strict LSP, and using specific preconditions gives you a way to get that when needed. But of course, in that case, dispatching calls may fail for no reason visible at the point of the call. (LSP = Liskov Substitutability Principle). > What if a sub-program expects a a class wide type with a root type and its > precondition, and get a derived type with a specific precondition it can't > know about? You still evaluate the specific precondition associated with the subprogram that is actually called. My understanding is that a lot of GNAT users only use carefully written specific preconditions (probably because they learned how to do that before class-wide preconditions existed in GNAT). Those can be, but don't have to, follow LSP. OTOH, class-wide preconditions follow LSP by design. My rule of thumb is that in a given derivation chain, you should only use one or the other. (I wanted to make that a requirement, but that was shot down.) I think given the sorts of programs that you write, you should only use class-wide preconditions and postconditions, and forget that specific ones exist at all. In which case, you won't have a problem with LSP. Randy.