Re: Press Release - Ada 2012 Language Standard Approved by ISO

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> 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.