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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,6327f05d4989a68d X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.180.97.198 with SMTP id ec6mr8399726wib.5.1356837412330; Sat, 29 Dec 2012 19:16:52 -0800 (PST) Path: i11ni337233wiw.0!nntp.google.com!feeder3.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feed.tweaknews.nl!216.196.110.142.MISMATCH!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!newsreader4.netcologne.de!news.netcologne.de!news.swapon.de!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Press Release - Ada 2012 Language Standard Approved by ISO Date: Sat, 22 Dec 2012 10:02:59 +0100 Organization: cbb software GmbH Message-ID: <1drh1q1ln2dfh$.a9hwlg01fjfy.dlg@40tude.net> References: <7wrdmbre6jw9.qww9l0uzj6mg.dlg@40tude.net> <14oqoq06zhlu2.tcasif3hdyhw.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: 6/SyjDFvQ5V7ZR2+GYgbDQ.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-12-22T10:02:59+01:00 List-Id: On Fri, 21 Dec 2012 19:40:57 -0600, Randy Brukardt wrote: > "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. We mean different "checks" here. As you have explained below, you mean a "true" check, a thing that never fails. I meant a dynamic check, a thing that is not statically true and need to be approached in the implementation according to the outcome. That evil thing is to be eliminated by introducing good things, "true checks." >> 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. procedure Foo (S : String) is subtype I is Integer range S'Range; >> 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. Ah, but we are in a full agreement here. What I said was: IF a "check" is dynamic THEN that must be an implementation. Since a true check may not fail. Then a fluttering "check" is something else. Bug, or an intended behavior, it is a part of the implementation. > 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). OK, this is rather a tactical disagreement then. Ada's stance was conservative, not eager adding features impossible to implement properly. Because somebody (Georg) could readily base his design on the faulty. In the first step I would rather prefer means to declare user-defined operations pure, context-dependent pure, compile-time evaluated etc. This would be more universal than mere predicates, and "proper" predicates would require that stuff anyway. An alternative, letting the compiler/vendor to deduce such properties, is IMO unrealistic (an undecidable problem, I think). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de