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: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.193.129 with SMTP id ho1mr764936pbc.8.1340310243954; Thu, 21 Jun 2012 13:24:03 -0700 (PDT) MIME-Version: 1.0 Path: l9ni4376pbj.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!news.stack.nl!nuzba.szn.dk!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Thu, 21 Jun 2012 15:23:57 -0500 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 1340310242 12574 69.95.181.76 (21 Jun 2012 20:24:02 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 21 Jun 2012 20:24:02 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-RFC2646: Format=Flowed; Response Date: 2012-06-21T15:23:57-05:00 List-Id: "Nasser M. Abbasi" wrote in message news:jrsjr7$uuo$1@speranza.aioe.org... ... > ----------------------------- > pragma Assertion_Policy(Check); > > procedure Push(S: in out Stack; X: in Item) > with > Pre => not Is_Full(S), > Post => not is Empty(S); > is > .... > end Push; > --------------------- > > One thing to notice right away, is that the pre/post checks > can be disabled or enabled by the pragma. Yes, but this is not a problem if you are careful. Specifically, your packages should at least contain pragma Assertion_Policy (Pre => Check, Pre'Class => Check, Static_Predicate => Check, Dynamic_Predicate => Check); (That is, all of the "inbound" assertion checks.) Then, the only way for someone to ignore these checks is to edit the source code of your library. If they do that, they've clearly "violated the warranty", and you have no obligation to make the body do anything useful if they do that. [Aside: note that assertions are "ignored", not "suppressed". The difference is that suppressed checks can still be made; it is only a permission to the compiler, not a requirement; ignored checks cannot be made.] This was a major topic of the Texas ARG meeting (the last one mainly about Ada 2012), and the above is the solution that we came up with. Note that there was a *lot* of discussion and opinion on this topic. Some people felt that any time someone ignores checks, that the program is erroneous and there ought to be no expectation that it works (if the checks would fail). Others (including me) felt that adding erroneous behavior because you added something that was supposed to make the program safer was nonsensical. ... > So, what is one to do? use pre/post AND also add > an extra check for full stack in the code as before? > does not make sense. Do as above. Force "inbound" checks to always be on (there is no need to leave "post" and "invariant" on, they only can fail due to a bug in your own code, not by anything that the caller can do). Randy.