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!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.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: Mon, 19 Dec 2016 16:52:45 -0600 Organization: JSA Research & Innovation Message-ID: References: NNTP-Posting-Host: rrsoftware.com X-Trace: franka.jacob-sparre.dk 1482187965 22167 24.196.82.226 (19 Dec 2016 22:52:45 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Mon, 19 Dec 2016 22:52:45 +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:32915 Date: 2016-12-19T16:52:45-06:00 List-Id: "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. 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. > 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. Can't see how it would be otherwise. The proof of a call, OTOH, need only take into account whatever is in the specification of the called routine. Otherwise, one has given up on separation of implementation for the purposes of proof (and proof can only then be done on completed programs, too late in the development cycle to be practical). But so far as I can tell, it doesn't matter much what is in the specification and what is in the body, just so that there is a good definition of which belongs to each. > 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 not in terms of proof. (And initialization, finalization, and aggregates are not extensible in Ada, at least not in any significant way. Anything that might cause trouble has to be written explicitly, and then we're just back to the normal case.) Randy.