Re: Preconditions which anyway would be caught?

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 14-08-09 22:24 , Peter Chapin wrote:
> On 2014-08-09 15:21, Peter Chapin wrote:
> 
>> Proper syntax here is
>>
>> function Inverse(X : Float)
>>   with Pre => (X /= 0) is
>> begin
>>    return 1/X;
>> end;
> 
> Well that's closer. How about
> 
> function Inverse(X : Float) return Float
>   with Pre => (X /=0) is
> begin
>    return 1/X;
> end;

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?

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .