Re: Hi-Lite high integrity showcase and overflow errors

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

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?