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,6327f05d4989a68d X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.180.97.198 with SMTP id ec6mr3102927wib.5.1356140460373; Fri, 21 Dec 2012 17:41:00 -0800 (PST) MIME-Version: 1.0 Path: i11ni250672wiw.0!nntp.google.com!goblin3!goblin.stu.neva.ru!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Press Release - Ada 2012 Language Standard Approved by ISO Date: Fri, 21 Dec 2012 19:40:57 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <7wrdmbre6jw9.qww9l0uzj6mg.dlg@40tude.net> <14oqoq06zhlu2.tcasif3hdyhw.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1356140459 30096 69.95.181.76 (22 Dec 2012 01:40:59 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 22 Dec 2012 01:40:59 +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: 2012-12-21T19:40:57-06:00 List-Id: "Dmitry A. Kazakov" wrote in message news:14oqoq06zhlu2.tcasif3hdyhw.dlg@40tude.net... ... > In essence 1 and 2 are about knowing something statically, during > compilation. Not necessarily the constraint itself, which may be dynamic, > yet allowing to prove something statically, e.g. that array index is > always > within the bounds. Well, I obviously disagree about that. Constraints, in my view are all about *introducing* checks. Predicates just provide an extension of that. > I don't see how predicates might be helpful for either 1 or 2. I don't see how range constraints would be helpful for either 1 or 2. > subtype Even is Positive with Dynamic_Predicate => Even mod 2 = 0; > subtype Each_Second_Character is String (Even); > > won't work. What I see is a yet another way to pack implementations into > declarations as Georg promptly suggested, a slippery slope... You believe checks are part of the implementation, while I believe that they are something separate. There is is no real hope of agreement on that, so I fear there isn't much point in discussing it. But I'll try for a moment... Checks, in my view, are things that should never fail in a correct program. Thus, they should not be considered part of the implementation; they're something separate. Indeed, the only reason that they are made dynamically is because checking them statically is beyond the current state of the art. (I would hope that by the time the next version of Ada rolls around, that will no longer be true.) Your argument about them being part of the implementation comes from the fact that Ada confuses the role of exceptions and handlers that come from checks vs. those that are part of the semantics (like End_Error). IMHO, it's wrong to be handling exceptions raised by checks; these represent bugs and must be eliminated from the program, not handled. (Handling them just covers up bugs.) For Ada 2012, you can differentiate exceptions somewhat by what is present in constract aspects (preconditions, predicates, etc.) - which always represent checks, but of course that's not quite complete. And there is a similar problem for handlers: there are "last chance" handlers (which capture all exceptions outbound), these aren't clearly separated from those handlers which are semantic in nature. Last chance handlers are necessary for all exits, of course, but they have nothing to do with the failed check (the check remains failed at the end of such a handler) . (GNAT does this better with their "at end" handler, but of course that's not Ada.) These are language flaws, not fundamental to the model. In an ideal world, all of these "checks" will get made statically. Hopefully that's coming. In mean time, it's important to get programmers used to the idea of writing checks this way, so that future tools can make the checks statically (there is no hope of making checks statically if they are just written in natural language comments). Randy.