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: Fri, 16 Dec 2016 21:14:46 +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-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32889 Date: 2016-12-16T21:14:46+01:00 List-Id: On 2016-12-16 20:46, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:o309ac$1f4q$2@gioia.aioe.org... >> On 15/12/2016 23:24, Randy Brukardt wrote: >>> "Dmitry A. Kazakov" wrote in message >>> news:o2tlcd$1aro$2@gioia.aioe.org... >>>> On 14/12/2016 23:40, Randy Brukardt wrote: >>>>> [Yet again had to break the thread because the thread has gotten too >>>>> long >>>>> to >>>>> reply to - RLB] >>>>> >>>>> "Dmitry A. Kazakov" wrote in message >>>>> news:o2s8l1$1fef$1@gioia.aioe.org... >>>>>> On 2016-12-14 20:23, Shark8 wrote: >>>>> ... >>>>>>> You are observably wrong. >>>>>>> If you supply a negative number, the body of X never executes. >>>>>> >>>>>> Of course it does. Semantically any effect of a call to X is due to >>>>>> X's body. There is nothing else there. >>>>> >>>>> This is clearly false. The definition of the execution of a subprogram call >>>>> (RM 6.4(10/2)) specifically says that the parameter associations are >>>>> evaluated before the subprogram body is executed. 6.4.1 says that >>>>> evaluation of the parameter associations include the conversion to the formal >>>>> subtype - that conversion does the check that raises Constraint_Error. >>>> >>>> And semantically all this is a part of the body. >>> >>> 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. This is especially important for correctness proofs. A proof must take into account *all* body. The user body part is not enough. 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... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de