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-7-bit Received: by 10.68.219.170 with SMTP id pp10mr12974766pbc.1.1341576477546; Fri, 06 Jul 2012 05:07:57 -0700 (PDT) Path: l9ni11017pbj.0!nntp.google.com!news2.google.com!goblin1!goblin.stu.neva.ru!noris.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Fri, 06 Jul 2012 14:07:52 +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: <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net> <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net> <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> In-Reply-To: <1l7pg7ihwb9vn$.kq6k3ypjwl07.dlg@40tude.net> Message-ID: <4ff6d51a$0$9514$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 06 Jul 2012 14:07:54 CEST NNTP-Posting-Host: b8ec1fe3.newsspool1.arcor-online.net X-Trace: DXC=8XgPfA>`ZDZYI9]OHn9o5^ic==]BZ:af^4Fo<]lROoRQnkgeX?EC@@PjD]=Ch2TYTRnc\616M64>ZLh>_cHTX3j]_]Hem@VihPU X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2012-07-06T14:07:54+02:00 List-Id: On 06.07.12 11:01, Dmitry A. Kazakov wrote: > On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote: > >> On 06.07.12 10:05, Dmitry A. Kazakov wrote: >>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: >>> >>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote: >>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >>>>> >>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>>>>> >>>>>>> Putting it even simpler. What is the effect of: >>>>>>> >>>>>>> sqrt (-1.0) >>>>>>> >>>>>>> No effect? Any effect? >>>>>> >>>>>> This looks like an imaginary problem to me, not a real one. >>>>> >>>>> What problem? It was a simple question illustrating absurdity of the idea. >>>> >>>> Actually, a negative argument passed to sqrt is illustrating proper DbC >>>> well. One famous example is Ariane 4, (4), that's the number four. >>> >>> If sqrt (-1.0) has no effect, >> >> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur. > > 1. That no correct program may have it requires a proof. Yes, this is why DbC is associated with a proof obligation. > 2. That no program at all may have it, requires yet another proof. Who cares? I mean, really, who cares? Assertion checking is *not* the same as showing that there exists a class of programs written in a suitably restricted language that is free of a number of possible errors. It is about programmers expressing things not expressible in Ada's type system. And DbC is about two parties, not just one. > 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. >>> what made Ariane to explode? >> >> The engineers though the didn't have to re-read the contract >> for Ariane 4 when moving the software to Ariane 5. > > But that has no effect or else does not occur... thus it never exploded. "That" = the contract? If a program is correct, then checking contract clauses does not have adverse effects. If a program is incorrectly calling sqrt with a negative argument, there are two practical cases 1) [wrong -1.0 and checks on] detects violation, restarts if possible 2) [wrong -1.0 and checks off] whatever sqrt's body does Both situations can make the system crash, because it might not be possible to retry using another, fresh value for r in case 1). Some have expressed a preference for detection (1) over erratic performance (2). I'll note in passing that a check is *not* testing I/O values. By the Ariane analogy, the original *system* was assumed, correctly, to guarantee that r >= 0.0. But another, different assembly of a new system rendered the guarantee void, introducing an explosive bug.