Re: Preconditions which anyway would be caught?

[Peter Chapin <PChapin@vtc.vsc.edu>]

On 2014-08-09 17:04, Niklas Holsti wrote:

> Just to be a pedant: shouldn't that have some decimals on the literals:
> 
> function Inverse(X : Float) return Float
>   with Pre => (X /= 0.0) is
> begin
>   return 1.0/X;
> end;
> 
> In addition, is it really true that all Float numbers /= 0.0 can be
> inverted without error? What if X is a denormalized number which has
> suffered gradual underflow... won't its inverse overflow, because there
> is no concept of "gradual overflow" in IEEE floats?

I wondered about that also, in fact.

I just tried it with your corrections so it actually *does* compile.
Without any precondition SPARK 2014 complains that

	overflow check might fail
	divide by zero check might fail

With the precondition of X /= 0.0 SPARK says

	overflow check might fail

However, this proves fine:

   function Inverse(X : Float) return Float
     with Pre => not(-1.0E-35 < X and X < +1.0E-35) is
   begin
      return 1.0/X;
   end;

I didn't experiment to see how close to zero I could make the bounds in
the precondition but clearly your concern is a valid one.

Peter