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.75.8 with SMTP id y8mr2378631wiv.1.1361848953561; Mon, 25 Feb 2013 19:22:33 -0800 (PST) Path: g1ni33259wig.0!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feeder3.cambriumusenet.nl!feed.tweaknews.nl!216.196.110.142.MISMATCH!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!news.teledata-fn.de!weretis.net!feeder4.news.weretis.net!news.mixmin.net!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Class wide preconditions: error in GNAT implementation? Date: Mon, 18 Feb 2013 09:30:16 +0100 Organization: cbb software GmbH Message-ID: <1hjhzbhx5ryn7$.rst5open618c.dlg@40tude.net> References: <30edd381-7505-496a-99e5-f884faf33c33@googlegroups.com> <16s3mt7cm3n61$.8qu6fp1nglfq.dlg@40tude.net> <1a648dqoysnp4$.7l9zsp043d2e.dlg@40tude.net> <377a4b9b-eec8-4af9-af3f-fdeb008339e4@googlegroups.com> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.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-18T09:30:16+01:00 List-Id: On Sat, 16 Feb 2013 11:55:55 -0800 (PST), ytomino wrote: > On Sunday, February 17, 2013 1:35:12 AM UTC+9, Dmitry A. Kazakov wrote: >> 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. > > Yes. *only the first one* = only As.foo'Pre'Class should be satisfied. No, all preconditions must be satisfied, otherwise, the program is incorrect, provided it is correctness we are talking about. >>>> 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. > > Are you imagining the dispatcher like below? > > procedure foo_Dispatcher (Object : A'Class) is > begin > pragma Assert (As.foo'Pre'Class); > case Object'Tag is > when A'Tag => > As.foo (A (Object)); > when B'Tag => > pragma Assert (Bs.foo'Pre'Class); -- unnecessary because weaker > Bs.foo (B (Object)); > ... > end case; > end foo_Dispatcher; > > If it is, your understanding is same as mine. But then the precondition of B'Class is *required* to be true for an object which is in that class. The precondition of A'Class is weaker and need not to be checked if one for B'Class is satisfied. > I'll repeat what I said. I believe the specification in Ada RM(AARM) is right > and merely point out the error in the behavior of GNAT. > The behavior of GNAT is different from what you says. I don't know. From the POV of correctness check, GNAT's behavior is perfectly OK. This only shows how dangerous it is to confuse checks with program semantics. Any program that rely on an outcome of a correctness check is automatically illegal. Yours already is since it prints from "checks." -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de