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=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.241.162 with SMTP id wj2mr14900375pbc.2.1341624286937; Fri, 06 Jul 2012 18:24:46 -0700 (PDT) MIME-Version: 1.0 Path: l9ni11017pbj.0!nntp.google.com!news2.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.ecp.fr!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Fri, 6 Jul 2012 20:24:39 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net> <33crfw5vkxoh$.kz5mq75s36ee.dlg@40tude.net> <43e4637c-3337-4d99-be45-20e054e5a203@googlegroups.com> <6ua1uo9zmkjn$.1tmqyzmetx71u$.dlg@40tude.net> <4ff6969e$0$9514$9b4e6d93@newsspool1.arcor-online.net> <1xkiqefb6watw.10fvt344m3c4g$.dlg@40tude.net> <4ff6a20a$0$9525$9b4e6d93@newsspool1.arcor-online.net> <1l7pg7ihwb9vn$.kq6k3ypjwl07.dlg@40tude.net> <4ff6d51a$0$9514$9b4e6d93@newsspool1.arcor-online.net> <7xnkuta2d94n$.1815f9iev4s7r$.dlg@40tude.net> <4ff7139f$0$9522$9b4e6d93@newsspool1.arcor-online.net> <80rid9aui8jv$.wg3phwexxdfy$.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1341624284 23477 69.95.181.76 (7 Jul 2012 01:24:44 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 7 Jul 2012 01:24:44 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-07-06T20:24:39-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:80rid9aui8jv$.wg3phwexxdfy$.dlg@40tude.net... ... > 1. Wrong. An exception is still there. Sure, but the compiler can prove that it will not be raised (at least part of the time). The Sqrt in the LRM has not such possibility; a caller would always have to assume that it is raised. >> but (2) we cannot really see from sqrt's specification what to do in >> order to avoid them, > > 2. Wrong, it is clearly seen from the post-condition It was clear as mud to me. Pre => (if A < 0.0 then raise Constraint_Error); is a *lot* clearer to me. >> and (3) we cannot have an efficient sqrt because Ada's sqrt forces >> a test on us that is quite unnecessary once we know, i.e. have shown, >> that x >= 0.0 is always true before calling sqrt. > > 3. Wrong. There is no whatsoever difference to dynamic check in that > respect. The implementation is same. That is BTW why there is no such > thing > as "dynamic check." And surely the second part of the postcondition can be > ignored if proven that X > 0.0, which would let the optimizing compiler to > deploy a modified body without check. Definitely wrong. Any decent compiler will completely eliminate the dynamic check on the precondition given above (presuming the actual value allows that). (Preconditions are checked at the call site, not inside the body.) No compiler can eliminate a dynamic check written in a body. So the generated code will be very different. Randy.