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.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC 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.227.67 with SMTP id ry3mr14071249pbc.8.1341602304587;
        Fri, 06 Jul 2012 12:18:24 -0700 (PDT)
Path: 
 l9ni11004pbj.0!nntp.google.com!news1.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!news.mixmin.net!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: about the new Ada 2012 pre/post conditions
Date: Fri, 6 Jul 2012 21:18:13 +0200
Organization: cbb software GmbH
Message-ID: <80rid9aui8jv$.wg3phwexxdfy$.dlg@40tude.net>
References: <jrsjr7$uuo$1@speranza.aioe.org>
 <Pine.LNX.4.64.1206251438390.12735@medsec1.medien.uni-weimar.de>
 <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net>
 <Pine.LNX.4.64.1206251734140.12735@medsec1.medien.uni-weimar.de>
 <bdpvyb9h7rvt.zbq0kbiq72wj.dlg@40tude.net>
 <Pine.LNX.4.64.1206261316320.22921@medsec1.medien.uni-weimar.de>
 <xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net> <jstvu4$jh4$1@munin.nbi.dk>
 <a555h2psfssb$.1be3awg0xbewa.dlg@40tude.net> <jt2rjm$vhe$1@munin.nbi.dk>
 <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>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: 9A8bJrx4NhDLcSmbrb6AdA.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: 8bit
Date: 2012-07-06T21:18:13+02:00
List-Id: <comp.lang.ada>

On Fri, 06 Jul 2012 18:34:37 +0200, Georg Bauhaus wrote:

> On 06.07.12 15:37, Dmitry A. Kazakov wrote:
> 
>    function sqrt (x : REAL) return REAL
>      with   Pre => True
>           Post  => sqrt'result * sqrt'result = x � eps or else *@$!;

Post =>
   (  X'Valid
   and then
      X >= 0.0
   and then
      (  sqrt'Result * sqrt'Result = X
     or else
         (  sqrt'Result * sqrt'Result > X
        and then
            sqrt'Result * sqrt'Result = X'Succ
         )
     or else
         (  sqrt'Result * sqrt'Result < X
        and then
            sqrt'Result * sqrt'Result = X'Pred
   )  )  )
or else
   (  (not X'Valid or else X < 0.0)
   and then
      Constraint_Error raised
   );

> instead, then (1) we not only have to handle exceptions,

1. Wrong. An exception is still there.

> 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

> 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.

See, doing things properly is always safer and no less efficient.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de