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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Tue, 6 Dec 2016 17:09:28 -0600 Organization: JSA Research & Innovation Message-ID: References: <92ed75e9-baae-455c-9e34-53348dc6eaef@googlegroups.com> <03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com> <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com> <47366b42-c0a3-41bf-a44a-5241c109d60f@googlegroups.com> NNTP-Posting-Host: rrsoftware.com X-Trace: franka.jacob-sparre.dk 1481065724 21060 24.196.82.226 (6 Dec 2016 23:08:44 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 6 Dec 2016 23:08:44 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Response X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:32643 Date: 2016-12-06T17:09:28-06:00 List-Id: "Dmitry A. Kazakov" wrote in message news:o24of4$1n05$1@gioia.aioe.org... > On 2016-12-05 12:09, Simon Wright wrote: ... >> Just as bad a thing as Constraint_Error. > > Not at all. Constraint_Error is defined and *desired* behavior. Exceptions > from pre-/post-conditions is undefined behavior. Why? Consider (part of) the procedure Delete in the Map container: procedure Delete (Container : in out Map; Position : in out Cursor); -- If Position equals No_Element, then Constraint_Error is propagated. As you say, this is defined and desired behavior. Now, consider a better (IMHO) definition of this definition: procedure Delete (Container : in out Map; Position : in out Cursor) with Pre => (if not Has_Element (Position) then raise Constraint_Error); Here, instead of using an English comment to define this behavior, we've used an Ada precondition. So what's undefined about this? It's exactly the same semantics, and indeed my hope is that we update the RM to do this for all of the container routines in Ada 202x. (That makes the description of the primary function of the routine much easier to find, because it gets rid of all of the special conditions that start most of those descriptions. And it should make static analysis easier as well.) IMHO, this is the only sensible use of a precondition (that is, it is some function of the parameters of the routine); it surely looks as defined as any if statement (which is what it would have to be written as in pre-Ada 2012). Randy.