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: a07f3367d7,834610f4f567e94b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.66.74.40 with SMTP id q8mr1830879pav.19.1347134001666;
        Sat, 08 Sep 2012 12:53:21 -0700 (PDT)
Path: 
 a8ni23310698pbd.1!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!ctu-peer!news.nctu.edu.tw!goblin1!goblin3!goblin.stu.neva.ru!news-2.dfn.de!news.dfn.de!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: Wed, 05 Sep 2012 13:15:56 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:15.0) Gecko/20120824 Thunderbird/15.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Hi-Lite high integrity showcase and overflow errors
References: <5045278b$0$6576$9b4e6d93@newsspool3.arcor-online.net>
 <9f990735-e6ca-43b3-9be5-930e8184626a@googlegroups.com>
In-Reply-To: <9f990735-e6ca-43b3-9be5-930e8184626a@googlegroups.com>
Message-ID: <50473468$0$6548$9b4e6d93@newsspool4.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 05 Sep 2012 13:15:52 CEST
NNTP-Posting-Host: b204b8b1.newsspool4.arcor-online.net
X-Trace: 
 DXC=b8<5EolXE74RadXUBHgFh34IUK<Cl32<14Fo<]lROoR18kF<OcfhCO;0cGjm6MEWa6nc\616M64>:Lh>_cHTX3j=R<@7oH9TFI8
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Date: 2012-09-05T13:15:52+02:00
List-Id: <comp.lang.ada>

On 05.09.12 11:19, yannick.moy wrote:
> One advantage of the new Ada 2012 executable annotations is that you can execute preconditions, which would catch the problem at the caller site.

Thanks for explaining. I'll assume, though, that for saturating
arithmetic, the caller would not want X op Y < 10_000 to be
checked as a precondition, as this prevents saturation. So the
postconditions are fine.