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,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.224.175.65 with SMTP id w1mr1916929qaz.7.1360900532229; Thu, 14 Feb 2013 19:55:32 -0800 (PST) X-Received: by 10.49.12.238 with SMTP id b14mr37809qec.18.1360900532210; Thu, 14 Feb 2013 19:55:32 -0800 (PST) Path: k2ni33058qap.0!nntp.google.com!t1no949568qaz.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 14 Feb 2013 19:55:32 -0800 (PST) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=122.17.51.175; posting-account=Mi71UQoAAACnFhXo1NVxPlurinchtkIj NNTP-Posting-Host: 122.17.51.175 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Class wide preconditions: error in GNAT implementation? From: ytomino Injection-Date: Fri, 15 Feb 2013 03:55:32 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2013-02-14T19:55:32-08:00 List-Id: Hello. I read https://groups.google.com/d/topic/comp.lang.ada/03cKrGghF2Y/discussi= on and recall a related question. See below example: package preconds is package Tools is function Write_In_Expr (S : String) return Boolean; -- Put_Line (S) a= nd return True end Tools; package As is type A is tagged null record; procedure foo (Object : A) -- empty body with Pre'Class =3D> Tools.Write_In_Expr ("A, in!"), Post'Class =3D> Tools.Write_In_Expr ("A, out!"); end As; package Bs is type B is new As.A with null record; overriding procedure foo (Object : B) -- empty body with Pre'Class =3D> Tools.Write_In_Expr ("B, in!"), -- [*] Post'Class =3D> Tools.Write_In_Expr ("B, out!"); end Bs; end preconds; with preconds; use preconds; procedure precondmain is x : access As.A'Class :=3D new Bs.B; begin As.foo (x.all); -- dispatching call as A'Class end precondmain; % gnatmake -gnat2012 -gnata precondmain.adb % ./precondmain B, in! B, out! A, out! And change [*] to Pre'Class =3D> Tools.Write_In_Expr ("B, in!") and False, % gnatmake -gnat2012 -gnata precondmain.adb % ./precondmain =20 B, in! A, in! B, out! A, out! It seems that the preconditions were evaluated as pragma Assert (B'Pre'Clas= s and then A'Pre'Class); By the way, AARM 6.1.1 38.a/3-b/3 says > Ramification: For a dispatching call, we are talking about the Pre'Class(= es) that apply to the subprogram that the dispatching call is resolving to,= not the Pre'Class(es) for the subprogram that is ultimately dispatched to.= The class-wide precondition of the resolved call is necessarily the same o= r stronger than that of the invoked call. For a statically bound call, thes= e are the same; for an access-to-subprogram, (which has no class-wide preco= nditions of its own), we check the class-wide preconditions of the invoked = routine.=20 >Implementation Note: These rules imply that logically, class-wide precondi= tions of routines must be checked at the point of call (other than for acce= ss-to-subprogram calls, which must be checked in the body, probably using a= wrapper). Specific preconditions that might be called with a dispatching c= all or via an access-to-subprogram value must be checked inside of the subp= rogram body. In contrast, the postcondition checks always need to be checke= d inside the body of the routine. Of course, an implementation can evaluate= all of these at the point of call for statically bound calls if the implem= entation uses wrappers for dispatching bodies and for 'Access values. I think(hope), this two lines mean only A'Pre'Class should be evaluated in = this case. B'Pre'Class should not be evaluated in this case. Isn't it? P.S. dmd (D language compiler) had same error. Its discussion may help for = reference. http://d.puremagic.com/issues/show_bug.cgi?id=3D6857