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, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,df055ffdd469757d X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.180.102.69 with SMTP id fm5mr4463714wib.0.1361288832804; Tue, 19 Feb 2013 07:47:12 -0800 (PST) Path: g1ni20557wig.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!194.109.133.87.MISMATCH!newsfeed.xs4all.nl!newsfeed1.news.xs4all.nl!xs4all!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!news.thorslund.org!news.jacob-sparre.dk!hugin.jacob-sparre.dk!nuzba.szn.dk!pnx.dk!news.stack.nl!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Class wide preconditions: error in GNAT implementation? Date: Sat, 16 Feb 2013 17:35:12 +0100 Organization: cbb software GmbH Message-ID: <1a648dqoysnp4$.7l9zsp043d2e.dlg@40tude.net> References: <30edd381-7505-496a-99e5-f884faf33c33@googlegroups.com> <16s3mt7cm3n61$.8qu6fp1nglfq.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: TNGw0NoNrWqwYmfxAaSXHQ.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2013-02-16T17:35:12+01:00 List-Id: On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote: >>> In this case, the caller should keep As.foo'Pre'Class because calling As.foo. >> No, the caller shall satisfy the precondition of the callee. Regarding >> inheritance, a primitive operation (callee) may weaken the precondition it >> overrides. This is why logical disjunction apply, as Randy said. > > No. The caller is "client" of not Bs but As, in this case. The precondition of a dispatching call is one of the class. The precondition of the specific operation can be weaker. The precondition of a LSP subclass can be stronger. All three shall be satisfied by the caller, but only the first one is actually constraining for it, because the second two are automatically satisfied through the mechanism of dispatching call and type coercion. >> Considering individual terms of the disjunction, the caller is allowed to >> satisfy at least one of them to make the call valid. > > Imagine, the system is running correctly, but depending on weak precondition of the subclass. > On day, new subclass is introduced into this system. > This new subclass has strong precondition equally to the superclass. > But, existing callers is depending on weak one. > It's a bug of callers, not subclasses. It won't happen. A weakened precondition apply to the another caller, an imaginary polymorphic body which is called by the original caller. When you arrive into that body and go trough the tag-case, and are ready to call the specific body, then the precondition of the latter apply. Original caller has to satisfy the precondition of the operation it calls. For a dispatching operation it is one of the class. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de