## Problem in DOUBLE.floor

Expand Messages
• Hello SmallEiffel, When flooring the DOUBLE -2147483648.0, an exception is raised due to an postcondition failing: floor: INTEGER is -- Greatest integral value
Message 1 of 3 , Jul 1, 2000
• 0 Attachment
Hello SmallEiffel,

When flooring the DOUBLE -2147483648.0, an exception is raised due to an
postcondition failing:

floor: INTEGER is
-- Greatest integral value no greater than Current.
local
d: DOUBLE;
do
d := double_floor;
Result := d.truncated_to_integer;
ensure
result_no_greater: Result <= Current;
close_enough: Current - Result < one
end;

The value -2147483647.0 converts fine. I really don't care that much, but I
post this message in case this postcondition is incorrect and the
SmallEiffel team wants to change it a bit.

Groetjes,

Berend. (-:
• ... Shouldn t this have a precondition like require (Current = 0) implies (Current =
Message 2 of 3 , Jul 1, 2000
• 0 Attachment
On 01-Jul-00, Berend de Boer wrote:

> When flooring the DOUBLE -2147483648.0, an exception is raised due to an
> postcondition failing:
>
> floor: INTEGER is
> -- Greatest integral value no greater than Current.

Shouldn't this have a precondition like

require
(Current >= 0) implies (Current <= Maximum_integer.to_double)
(Current < 0) implies (Current >= Minimum_integer.to_double)

in other words: does the input result into something that can be expressed
as INTEGER? (Probably a -1 is missing somewhere in my suggestion...)

Interestingly, the various "other" short forms (ELKS95, ISE, OT) on the web
don't have this precondition. That means, the also produce wrong
results, or the raise some kind of overflow exception.

Regards,

Thomas.
• ... Simply require Current = Minimum_integer.to_double ... Just like C and most other languages. David
Message 3 of 3 , Jul 1, 2000
• 0 Attachment
> From: Thomas Aglassinger [mailto:agi@...]
> Shouldn't this have a precondition like
>
> require
> (Current >= 0) implies (Current <= Maximum_integer.to_double)
> (Current < 0) implies (Current >= Minimum_integer.to_double)

Simply
require
Current <= Maximum_integer.to_double
Current >= Minimum_integer.to_double

> in other words: does the input result into something that can be expressed
> as INTEGER? (Probably a -1 is missing somewhere in my suggestion...)
>
> Interestingly, the various "other" short forms (ELKS95, ISE, OT) on the web
> don't have this precondition. That means, the also produce wrong
> results, or the raise some kind of overflow exception.

Just like C and most other languages.

David
Your message has been successfully submitted and would be delivered to recipients shortly.