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.220.230 with SMTP id pz6mr16324190pbc.3.1341667958934;
        Sat, 07 Jul 2012 06:32:38 -0700 (PDT)
Path: 
 l9ni11068pbj.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!xlned.com!feeder1.xlned.com!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Sat, 07 Jul 2012 15:31:59 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
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: <jrsjr7$uuo$1@speranza.aioe.org>
 <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> <jt82pf$kbb$1@munin.nbi.dk>
 <79brat0uiqr5.s237scuc0h68$.dlg@40tude.net>
 <4ff82656$0$9521$9b4e6d93@newsspool1.arcor-online.net>
 <1lv4w2cek7j8k.c30ranmy8kg8.dlg@40tude.net>
In-Reply-To: <1lv4w2cek7j8k.c30ranmy8kg8.dlg@40tude.net>
Message-ID: <4ff83a50$0$9505$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 07 Jul 2012 15:32:00 CEST
NNTP-Posting-Host: a2c52d8d.newsspool1.arcor-online.net
X-Trace: 
 DXC=4MRa@[]H_n3QbA1[CgMQ00ic==]BZ:af>4Fo<]lROoR1nkgeX?EC@@08WEnDiKGIR2PCY\c7>ejV8fT71]<6`cN;0NiH]KT]OC8
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-07-07T15:32:00+02:00
List-Id: <comp.lang.ada>

On 07.07.12 14:54, Dmitry A. Kazakov wrote:
> On Sat, 07 Jul 2012 14:06:46 +0200, Georg Bauhaus wrote:
>
>> On 07.07.12 11:14, Dmitry A. Kazakov wrote:
>>> That the same function's behavior might be both defined and undefined.
>>
>> The function's behavior is not affected by assertion checking:
>
> Whatever it be. You wrote about the effect of sqrt exactly this:
>
> "the effect is similar to that of using Unchecked_Conversion."

Yes, the function's behavior is according to both sides of the
stated contract.

Continuing the Unchecked_Conversion analogy,
there are safe uses of Unchecked_Conversion. Improving Ada 2005,
a full DbC method allows formalizing these safe use cases to the extent
possible in each case. For example, it is safe to call sqrt if the caller
ensures the conditions stated in the explicit contract of my_sqrt.