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=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no 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 Received: by 10.68.196.232 with SMTP id ip8mr13618706pbc.6.1341592502980; Fri, 06 Jul 2012 09:35:02 -0700 (PDT) Path: l9ni11004pbj.0!nntp.google.com!news1.google.com!news.glorb.com!news2.arglkargh.de!noris.net!news.teledata-fn.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Fri, 06 Jul 2012 18:34:37 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:13.0) Gecko/20120614 Thunderbird/13.0.1 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions References: <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> <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> In-Reply-To: <7xnkuta2d94n$.1815f9iev4s7r$.dlg@40tude.net> Message-ID: <4ff7139f$0$9522$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 06 Jul 2012 18:34:39 CEST NNTP-Posting-Host: 5be61393.newsspool1.arcor-online.net X-Trace: DXC=6C\[;I^?]^e<6cDJZfMd_cic==]BZ:afn4Fo<]lROoRankgeX?EC@@`_VX:i1JEGkjnc\616M64>jLh>_cHTX3jm0_PAG<\T9mj X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Date: 2012-07-06T18:34:39+02:00 List-Id: On 06.07.12 15:37, Dmitry A. Kazakov wrote: >>> I'd rather stay on the safe side >>> >> considering sqrt (-1.0) happen. So, what about the effect? >> > >> > If you know that you might be running an incorrect program, >> > the effect is similar to that of using Unchecked_Conversion. > Maybe for Ada 202X, but in contemporary Ada it is Constraint_Error > propagation. Could you leave clauses of an explicitly state contract in the text where there was one? function sqrt (x : REAL) return REAL with Pre => x >= 0.0; Ada's sqrt, as opposed to the sqrt above, adds a run-time check, fully dynamic. The programmer can throw anything at Ada's sqrt, quite carelessly. Its contract isn't specified in source text, but requires that the programmer study the language manual in order to learn about his obligations, and possible consequences. When not, the program needs to handle Constraint_Error all over the place because he or she *never* knows what precondition to establish, other than by reading through more or less formal comments. Triply bad. If we had function sqrt (x : REAL) return REAL with Pre => True Post => sqrt'result * sqrt'result = x � eps or else *@$!; instead, then (1) we not only have to handle exceptions, but (2) we cannot really see from sqrt's specification what to do in order to avoid them, 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. So Ada's sqrt is programmed defensively, whereas the line of defence in a program designed by contract is to feel obliged by the contract and then either demonstrate correctness, or leave the checks in!