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!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Tue, 20 Dec 2016 11:59:52 +0100 Organization: Aioe.org NNTP Server Message-ID: References: NNTP-Posting-Host: s3c6wwRqkurrfTZpuYYZ+w.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Mozilla-News-Host: news://news.aioe.org X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32923 Date: 2016-12-20T11:59:52+01:00 List-Id: 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. > 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! >> 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 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... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de