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 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.180.75.8 with SMTP id y8mr4459362wiv.1.1361288832717; Tue, 19 Feb 2013 07:47:12 -0800 (PST) MIME-Version: 1.0 Path: g1ni20557wig.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.138.MISMATCH!xlned.com!feeder5.xlned.com!newsfeed.xs4all.nl!newsfeed3.news.xs4all.nl!xs4all!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!news.thorslund.org!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 GNAT implementation? Date: Fri, 15 Feb 2013 19:01:53 -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 1360976514 26591 69.95.181.76 (16 Feb 2013 01:01:54 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 16 Feb 2013 01:01:54 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2013-02-15T19:01:53-06:00 List-Id: "ytomino" wrote in message news:e155e2d6-ba1f-4fc0-a6e3-dafde002670b@googlegroups.com... ... >% gnatmake -gnat2012 -gnata precondmain.adb >% ./precondmain >B, in! >B, out! >A, out! > >And change [*] to Pre'Class => Tools.Write_In_Expr ("B, in!") and False, > >% gnatmake -gnat2012 -gnata precondmain.adb >% ./precondmain >B, in! >A, in! >B, out! >A, out! This looks right to me (well, actually not quite, see far below). >It seems that the preconditions were evaluated as pragma Assert >(B'Pre'Class and then A'Pre'Class); Class-wide Preconditions are combined with "or", not "and". And of course Once you get True for "or", you don't need to evaluate any more of them. See 6.1.1(33/3)- "if and only if all ... evaluated to False". The order of evaluation of these expressions is unspecified, so which one gets evaluated depends on the compiler. Postconditions (and specific preconditions) are combined with "and". The reasons for this are found in the theories of LSP. I could explain it, but it would take me all day, and you'd probably be more confused than you started. :-) (It took a long time for most of the ARG, me included, to understand this well enough to determine whether or not the features were properly defined.) OTOH, I didn't realize that you had a dispatching call. In that case, the precondition is supposed to just be the Pre'Class for A, which is stronger that A or B which a direct call would use. Probably GNAT dispatched and then checked the precondition. Technically, that's wrong (although I would have a hard time caring, the reason for the stronger precondition on dispatching calls is to allow analysis without knowing the actual tag, it doesn't have anything to do with correctness). Randy.