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.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham 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.66.84.38 with SMTP id v6mr1629564pay.32.1361044555631; Sat, 16 Feb 2013 11:55:55 -0800 (PST) X-Received: by 10.50.207.100 with SMTP id lv4mr607213igc.1.1361044555401; Sat, 16 Feb 2013 11:55:55 -0800 (PST) Path: ov8ni9pbb.1!nntp.google.com!su1no7679772pbb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sat, 16 Feb 2013 11:55:55 -0800 (PST) In-Reply-To: <1a648dqoysnp4$.7l9zsp043d2e.dlg@40tude.net> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=114.163.213.55; posting-account=Mi71UQoAAACnFhXo1NVxPlurinchtkIj NNTP-Posting-Host: 114.163.213.55 References: <30edd381-7505-496a-99e5-f884faf33c33@googlegroups.com> <16s3mt7cm3n61$.8qu6fp1nglfq.dlg@40tude.net> <1a648dqoysnp4$.7l9zsp043d2e.dlg@40tude.net> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <377a4b9b-eec8-4af9-af3f-fdeb008339e4@googlegroups.com> Subject: Re: Class wide preconditions: error in GNAT implementation? From: ytomino Cc: mailbox@dmitry-kazakov.de Injection-Date: Sat, 16 Feb 2013 19:55:55 +0000 Content-Type: text/plain; charset=ISO-8859-1 Date: 2013-02-16T11:55:55-08:00 List-Id: 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. > >> 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. 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.