Not a Number
If you are writing programs in an environment where NaNs (Not-a-Number) crop up a lot, as I am, then turning on assertion checking beyond require level is not, in general, practical. The problem is not performance, but the fact that no NaN compares equal to any number, including itself. And for good reason.
So when you encounter a postcondition such as this from class
put (v: like item; i: INTEGER_32) -- Replace `i'-th entry, if in index interval, by `v'. require -- from TABLE valid_key: valid_index (i) require -- from TO_SPECIAL valid_index: valid_index (i) do area.put (v, i - lower) ensure then -- from INDEXABLE insertion_done: item (i) = v ensure -- from TO_SPECIAL inserted: item (i) = v end
you will get a violation if
item is of type
REAL_64 (for instance), and
v is a NaN.
And such postconditions are pervasive.
This is a serious difficulty with Eiffel at the moment. So I am putting forward the following proposal as a starter to kick off a community discussion.
This will differ from
is_equal in that if either operand is a NaN, then the result is guaranteed to be False. Whereas
is_equal will return True if both operands are NaNs.
Now it is important that the
= operator can continue to be used in the traditional mathmatical sense for numbers. So it will have to differ in its definition for class
NUMERIC from all other classes. This will be a language change, since ECMA states that = uses is_equal.
This means that postcondition like:
insertion_done: item (i) = v
INDEXABLE need to be re-written to use