From: Niklas Holsti <niklas.holsti@tidorum.invalid>
Subject: Re: Preconditions which anyway would be caught?
Date: Sun, 10 Aug 2014 00:04:11 +0300
Date: 2014-08-10T00:04:11+03:00 [thread overview]
Message-ID: <c4nglvFm5o1U1@mid.individual.net> (raw)
In-Reply-To: <BJadnfLOjLUf6HvO4p2dnAA@giganews.com>
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
. @ .
next prev parent reply other threads:[~2014-08-09 21:04 UTC|newest]
Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-08-09 15:35 Preconditions which anyway would be caught? Victor Porton
2014-08-09 15:40 ` mockturtle
2014-08-09 16:08 ` Jeffrey Carter
2014-08-09 19:21 ` Peter Chapin
2014-08-09 19:24 ` Peter Chapin
2014-08-09 21:04 ` Niklas Holsti [this message]
2014-08-09 22:57 ` Peter Chapin
2014-08-10 20:58 ` Niklas Holsti
2014-08-10 7:24 ` Dmitry A. Kazakov
2014-08-11 0:00 ` Shark8
2014-08-11 7:31 ` Dmitry A. Kazakov
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox