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!gandalf.srv.welterde.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, 20 Dec 2016 18:50:02 -0600 Organization: JSA Research & Innovation Message-ID: References: NNTP-Posting-Host: rrsoftware.com X-Trace: franka.jacob-sparre.dk 1482281403 7239 24.196.82.226 (21 Dec 2016 00:50:03 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Wed, 21 Dec 2016 00:50:03 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-RFC2646: Format=Flowed; Response Xref: news.eternal-september.org comp.lang.ada:32929 Date: 2016-12-20T18:50:02-06:00 List-Id: "Dmitry A. Kazakov" wrote in message news:o3b2va$153k$1@gioia.aioe.org... > On 2016-12-19 23:52, Randy Brukardt wrote: >> "Dmitry A. Kazakov" wrote in message >> news:o31hvm$1p4s$1@gioia.aioe.org... >>> On 2016-12-16 20:46, Randy Brukardt wrote: >>>> "Dmitry A. Kazakov" 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.