PR# 19491 Postcondition of `twin' violated with NaN

The following code:

		local
			a, b: ANY
		do
			a := {REAL_64}.nan
			b := a

fails with this exception trace:

******************************** Thread exception *****************************
In thread           Root thread            0x0 (thread id)
*******************************************************************************
-------------------------------------------------------------------------------
Class / Object      Routine                Nature of exception           Effect
-------------------------------------------------------------------------------
REAL_64             twin @2                is_equal:
<00000241842B05F8>  (From ANY)             Postcondition violated.       Fail
-------------------------------------------------------------------------------
REAL_64             twin @2
<00000241842B05F8>  (From ANY)             Routine failure.              Fail
-------------------------------------------------------------------------------
GEPP                execute @2
<00000241842B05A8>                         Routine failure.              Fail
-------------------------------------------------------------------------------
GEPP                root's creation
<00000241842B05A8>                         Routine failure.              Exit
-------------------------------------------------------------------------------

--
Eric Bezault

The change that will follow solution C or D is planned for EiffelStudio 19.05 to prevent last minute breaking changes in 18.11. This will change the default of the option "total order on reals" for newly created projects. Old projects could still rely on the current behavior. However, the compiler will report a warning when "total order on reals" is set to False.

The current workaround is to set the option "total order on reals" to True for all projects explicitly.

In my opinion, variants A and B are a poor man's solution. The problem is in classes REAL_32 and REAL_64. So the fix should be applied in these classes, not in all possible clients of these classes. NaN is breaking Eiffel assertions even in these REAL classes. The invariant "recursive_equality" inherited from ANY is violated. Because of NaN we don't have the total order relation that is promised by the inheritance from COMPARABLE. From example:

    print ({REAL_64}.nan >= 3.0)
    print ({REAL_64}.nan.to_reference >= (3.0).to_reference)

the first one (everything built-in) returns False, the second one (using code inherited from COMPARABLE) returns True.

So I would favor variants C or D. But not only equality should be addressed but also comparison operators. And we should probably add:

    ieee_is_less alias "#<" (other: like Current): BOOLEAN

or something like that (and similar routines for the other comparison operators and equality) for the users who want to get the IEEE semantics.
Of cour
....
Output truncated, Click download to get the full message

Just to clarify, what are the suggestions


Variant A:

1) twin (and similar ones: clone, copy, etc.) should change
      Result ~ Current
into
      Current = Current implies Result ~ Current

2) all containers should change postconditions like
      item (...) = value
into
      value = value implies item (...) = value


Variant B (similar to KL_TYPE.same_objects of Gobo):

1) twin (and similar ones: clone, copy, etc.) should change
      Result ~ Current
into
      safe_equal (Result, Current)
where
      safe_equal will do internally the checks of variant A (or use the code similar to KL_TYPE.same_objects)

2) all containers should change postconditions like
      item (...) = value
into
      safe_equal (item (...), value)


Variant C:

The compiler always treats NaN values as equal.


Variant D:

The compiler treats bit-wise identical NaN values as equal.

A final remark: I made sure that the postconditions in the container classes of Gobo (such as "last = v" in routines like `put_last (v: G)') have been adapted to deal with this NaN issue.
Let's not put our heads in the sand and claim that it's because of IEEE and that there is an ECF option. If the assertions are broken, they are broken and they need to be fixed.

I should add that this case with the assertion violation in `twin' is particularly problematic since, because of the call to `twin' which happens behind the scene, one cannot have an assignment. 

Interestingly, only the second assignment triggers the postcondition violation. Isn't `twin' called when assigning an expanded to a reference?

I know all that. This is not my problem. This is yours. I got a postcondition violation in {REAL_64}.twin. This neither my class nor my routine. Either {REAL_64} should not allow NaN, and if it does, then EiffelBase's assertions should take that special case into account.

According to IEEE standard, NaN is not equal to NaN, thus the assertion violation. The option "Total order on REALs" can be turned on to disable this behavior and to consider NaN as equal to NaN:

   https://www.eiffel.org/doc/eiffelstudio/Advanced_Options

If the project uses a precompile, the precompile should be built with the same option. The project has to be rebuilt from scratch to take the new option value into account.

Feel free to close this problem report if you consider using the option as a satisfactory solution.