Re: Ada 2012 Constraints (WRT an Ada IR)

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o3b2va$153k$1@gioia.aioe.org...
> On 2016-12-19 23:52, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o31hvm$1p4s$1@gioia.aioe.org...
>>> On 2016-12-16 20:46, Randy Brukardt wrote:
>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> ...
>>>>>> I just quoted the rules in the RM that say specifically that it is 
>>>>>> not
>>>>>> part of the body.
>>>>>
>>>>> What the problem? There is time to fix the RM wording. Call it "user
>>>>> specified body" as opposed to the "body in effect".
>>>>
>>>> What possible good would it do?
>>>
>>> It would fix wrong wording and eliminate misunderstanding about the
>>> semantics of parameter checks and other prologues (and epilogues!) the
>>> compiler uses to decorate the user body.
>>
>> "Wrong wording"? You'd have to find some observable case of incorrect
>> behavior to make such a claim.
>
> You already did it. According to the wording there exist implementations 
> that do not raise Constraint_Error but being called still do (due to 
> "out-of-body experience" range check). This is a trivial contradiction.

I don't understand "but being called still do". In any case, a body is not 
called if evaluating the parameters raise an exception; a call (like 
everything else) is a multi-part process.

In any case, some part of the execution of a subprogram call has to be 
evaluated at the call site, since the details of the actual parameters 
cannot be part of the body (they'll be different for every call). And those 
evaluations can raise exceptions. So the only question is precisely where 
the line is drawn, and that is only important in that it is precisely 
defined - the exact definition doesn't matter.

To take an example. The rule is that all parameter expressions are 
implicitly converted to the type/subtype of the parameter in a call.

     X : constant Integer := 0;
    procedure Foo (P : Positive);

   Foo (10 / X); -- Clearly, the evaluation of the call raises 
Contraint_Error (for a divide-by-zero). The body never executes.

   Foo (Positive(X)); -- Clearly, the evalation of the call raises 
Constraint_Error (for a conversion failure). The body never executes.

   Foo (X); -- Raises Constraint_Error because the implicit conversion is 
the same as the explicit onew given above. Again, the body never executes.

My understanding is that the designers of Ada 83 wanted the semantics of the 
last two calls to be exactly the same, as the former is just the explicit 
version of the implicit conversion of the second call. It would be unusual 
if they executed differently at all. (On top of which, the rules for 
derivation include similar implicit conversions, and those conversions need 
to work the same as similar code written explicitly.) None of that has ever 
been changed since Ada 83.

...
>> So far as I can tell, only you have a
>> "misunderstanding about the semantics", since there is no such thing as
>> "decorating the user body". Some stuff happens at the call site before 
>> the
>> user body is invoked. Clearly some dynamic stuff has to be done there
>> (evaluation of actuals can't happen in the body for obvious reasons), and
>> where one draws the line is a matter of taste.
>
> Exactly this mess!

It has to be true, there is no alternative. You just want to move the line a 
bit, but there is no advantage to doing that. But it necessarily would 
produce worse code (an Ada compiler is not allowed to look into bodies 
outside of Inline), and it also would make implicit and explicit conversions 
work differently.

>>> This is especially important for correctness proofs. A proof must take
>>> into account *all* body. The user body part is not enough.
>>
>> A body proof surely has to take into account the body's specification.
>
> A specification that does not correspond to the implementation! According 
> to the wording, the specification tells it raises, and the "body" does 
> not.
>
>> Can't see how it would be otherwise.
>
> Elementary, the specification and the body must correspond each other.

And of course they do. Ada has rules that require them to be exactly the 
same. So what? Some rules are checked before the actual call is made, and 
some after. All that is important is that which are checked where are 
well-defined. It's impossible to check all rules at one place or the other.

>>> And with extensible bodies (as required by initialization, finalization
>>> and aggregates) and the gluing code between them I don't know how are 
>>> you
>>> going to maintain this silly concept further...
>>
>> I don't follow this at all. There's nothing different about the built-in
>> extensions (mostly streams) from any other subprogram.
>
> Certainly checks decorating user-defined bodies of stream attributes for 
> some components may raise something. According to the nonsense you are 
> defending, these would not be the result of the body, being propagated 
> right from the middle of its execution...

The result of *which* body? In this case, (as in all cases involving 
implicit things) there are implicit calls of the original bodies. There's no 
actual combining of routines (that would be problematic both semantically 
and implementationally). And of course implicit calls follow the rules of 
other calls.

                               Randy.