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.190.104 with SMTP id gp8mr12893679pbc.4.1341574416039; Fri, 06 Jul 2012 04:33:36 -0700 (PDT) Path: l9ni11017pbj.0!nntp.google.com!news2.google.com!goblin3!goblin1!goblin.stu.neva.ru!eternal-september.org!feeder.eternal-september.org!mx04.eternal-september.org!.POSTED!not-for-mail From: Simon Wright Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Fri, 06 Jul 2012 12:33:33 +0100 Organization: A noiseless patient Spider Message-ID: 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> Mime-Version: 1.0 Injection-Info: mx04.eternal-september.org; posting-host="9/lhd+j3dpHAtSMlbElkYg"; logging-data="25395"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18dYPJZ0laaOb0dY1zZNzRJgn1fqGLlrGI=" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.1 (darwin) Cancel-Lock: sha1:DmpeVOhyqVZlirnZVUD4u2Pc2VY= sha1:tnPVnJLqxDzF/DnAC9N3Bj7Nef0= Content-Type: text/plain Date: 2012-07-06T12:33:33+01:00 List-Id: "Dmitry A. Kazakov" writes: > 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. If a DbC program passes a negative argument to sqrt(), then it isn't correct. To prove that a DbC program never passes a negative argument to sqrt() requires a proof (tautology). No proof is required of the statement that a correct program must not pass a negative argument to sqrt() - the contract must be regarded as axiomatic from the caller's pov. > 2. That no program at all may have it, requires yet another proof. I can't make sense of this statement. > 3. While you are busy proving 1 and 2, I'd rather stay on the safe side > considering sqrt (-1.0) happen. So, what about the effect? There will be an exception. What's the problem with that? In my last project, unhandled exceptions caused the system to be rebooted (and missiles in flight to be aborted). If the system throws an unhandled exception it's operating outside its design envelope and safety considerations come in to play.