Difference between revisions of "REAL 64 (issues)"

Revision as of 08:08, 27 November 2006

This page describes issues with the current implementation of REAL_64 in comparison to the interface description or desired output when nothing is specified.

is_equal and NaN

The floating point standard says that 'NaN = NaN' is false. But in order to uphold the postcondition of 'NaN.twin' which says that 'Result.is_equal (Current)' the comparison with 'is_equal' should yield true.

At the moment 'is_equal' for reals is optimized in the compiler and is replaced by '=' and thus the postcondition of 'twin' is violated.

floor, ceiling, rounded and truncated_to_integer

Currently when doing a 'floor', 'ceiling', 'rounded' or 'truncate_to_integer' with a number which is too large (e.g. 2^31) the result is {INTEGER}.min_value.

The change in the sign is a not expected behavior and violates informal contracts (see comments in EiffelBase REAL_64_REF.truncated_to_integer).

divisible

By providing NaN and INF every real value can be divided by every other real value. Thus a call of 'divisible' should always return true or the precondition of the division should be changed. This arises again in INTEGER.infix "/". A call to 12 / 0 is not allowed by the current contract but should just return INF.

inherited invariants

Some of the invariants which are inherited from NUMERIC are not applicable if the REAL is eithern NaN or INF. To circumvent this problem we could introduce a 'is_special_case' feature into NUMERIC and change the invariants form NUMERIC to be only true if the object is not a special case.

three_way_comparison

The postcondition of three_way_comparison is violated in the case where one object is infinity and the other object is NaN:

The postcondition lists the three cases of three_way_comparison. In the case where one of the two comparables is NaN and the other is INF, all three cases are violated. Thus the returning value should neither be -1, 0 or 1. Currently in this case 0 is returned which then violates the contract since NaN is not equal to infinity. What return value should be used is yet unclear. To uphold the contract it would be sufficent to return any number not equal to -1, 0 or 1. But this is more of a hack than a solution.