Difference between revisions of "REAL 64 (issues)"
m |
Colin-adams (Talk | contribs) (Mark Howard's proposal for dealing with NaNs) |
||
| (13 intermediate revisions by 3 users not shown) | |||
| Line 1: | Line 1: | ||
[[Category:ELKS]] | [[Category:ELKS]] | ||
| − | This page describes issues with the current implementation of REAL_64 in comparison to the [[REAL_64 (interface)| | + | This page describes issues with the current implementation of REAL_64 in comparison to the [[REAL_64 (interface)|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, 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 any other real value (including itself). 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. | ||
| + | |||
| + | In the C# implementation the return value of a three way comparison involving NaN returns always that NaN is smaller compared to any other real value except with NaN itself where it is equal. But when using the comparison operators, NaN compared to any other value is false. Thus this solution cannot be used to uphold the current contract from COMPARABLE. | ||
| + | |||
| + | The cleanest solution would be to introduce an 'is_special_case' feature in COMPARABLE like the one in NUMERIC. That way we could make the contract conditional on this feature. The downside is that you introduce COMPARABLE objects which are not comparable! (Although NaN is already an object which is a COMPARABLE but cannot be compared...) | ||
| + | |||
| + | ===A suggestion from Mark Howard=== | ||
| + | |||
| + | Mark Howard has told me that his idea to solve the NaN problem is to prefix assertions with "x=x implies ...". This works regardless of the type of object involved, so it is particularly useful in postconditions of routines such as extend. | ||
| + | This does not help for infinities, but I would have thought that this should be tackled by an is_infinite query in NUMERIC. | ||
| + | --[[User:Colin-adams|Colin-adams]] 08:55, 18 September 2007 (CEST) | ||
Latest revision as of 21:55, 17 September 2007
This page describes issues with the current implementation of REAL_64 in comparison to the interface description or desired output when nothing is specified.
Contents
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, 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 any other real value (including itself). 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.
In the C# implementation the return value of a three way comparison involving NaN returns always that NaN is smaller compared to any other real value except with NaN itself where it is equal. But when using the comparison operators, NaN compared to any other value is false. Thus this solution cannot be used to uphold the current contract from COMPARABLE.
The cleanest solution would be to introduce an 'is_special_case' feature in COMPARABLE like the one in NUMERIC. That way we could make the contract conditional on this feature. The downside is that you introduce COMPARABLE objects which are not comparable! (Although NaN is already an object which is a COMPARABLE but cannot be compared...)
A suggestion from Mark Howard
Mark Howard has told me that his idea to solve the NaN problem is to prefix assertions with "x=x implies ...". This works regardless of the type of object involved, so it is particularly useful in postconditions of routines such as extend. This does not help for infinities, but I would have thought that this should be tackled by an is_infinite query in NUMERIC. --Colin-adams 08:55, 18 September 2007 (CEST)
