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,UTF8
Received: by 10.66.82.195 with SMTP id k3mr4176127pay.23.1347464299799;
        Wed, 12 Sep 2012 08:38:19 -0700 (PDT)
Path: 
 a8ni20136626pbd.1!nntp.google.com!border1.nntp.dca.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!ctu-peer!news.nctu.edu.tw!goblin1!goblin.stu.neva.ru!news.osn.de!diablo2.news.osn.de!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 04 Sep 2012 10:30:49 +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>
 <269901b0-6570-4d7a-bcd4-19d590383515@googlegroups.com>
 <f9c3420e-7959-4ddf-b61c-d0eabbfdd197@googlegroups.com>
In-Reply-To: <f9c3420e-7959-4ddf-b61c-d0eabbfdd197@googlegroups.com>
Message-ID: <5045bc39$0$6569$9b4e6d93@newsspool3.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 04 Sep 2012 10:30:49 CEST
NNTP-Posting-Host: d44a90f9.newsspool3.arcor-online.net
X-Trace: 
 DXC=2D<Ko`DD:PB[kmHKHnaEnMMcF=Q^Z^V3H4Fo<]lROoRA8kF<OcfhCOKhN115;<XaX@PCY\c7>ejVH5k0eMiK[ogBJFFHGfn?ShA
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Date: 2012-09-04T10:30:49+02:00
List-Id: <comp.lang.ada>

On 04.09.12 05:05, Shark8 wrote:

> 	function Mult (X , Y : My_Int) return My_Int is
> 	begin
> 	    Return Result : My_Int do
> 		Result:= X*Y;
>
> 		-- When the constraint is exceeded we return the last value.
> 		exception
> 		when Constraint_Error =>
> 		    Result:= My_Int'Last;
> 	    End Return;
> 	end Mult;
>

Part of the exercise (which also mentions SPARK) is to have
programs that can drop support for exception handling, I should think.
Formally verified etc etc. So, no, this won't fly ;-)

When McJones & Stepanov introduced the idea behind their recent book
Stepanov has McJones put up a slide, titled "Respect the Domain", which
involves the quantity 2*b. The following lines are taken from near
00:41:45 of http://www.youtube.com/watch?v=Ih9gpJga4Vc:

   // Precondition: a ≥ b > 0
   if (a - b >= b) {  //! Not: a >= b + b

He points out that programmers need to work with potentially partial
functions; "+" is not everywhere defined; it can overflow.
We have to guard as in the Precondition, and "therefore, we could
subtract", even when most mathematicians would say this is stupid
(the meaning of the call-out bubble starting with //! above), which
it isn't because b + b might require more bits than are available.

That's much like X op Y in Hi-Lite's Mult/Add conditionals,
isn't it?