19 May 1997
Here's the question again:
What's wrong with this routine? It's supposed to print the object_id of two COMPARABLE objects in ascending comparable order (not ascending object_id order).
print_ascending(c1: COMPARABLE; c2: like c1) is
require
not_void: c1 /= void and c2 /= void
do
print( c1.min(c2).object_id.out )
print( c1.max(c2).object_id.out )
end
The "Gotcha" is that 'min' and 'max' both return 'current' when both objects have the same sorting order. So if c1 and c2 are comparably equal, the object-id for c1 will be printed twice.
For example, suppose we have a class TENNIS_PLAYER that inherits from COMPARABLE and redefines the comparison operators according to ranking order. Suppose we print 'name' rather than 'object_id'.
We then call "print_ascending(becker, navratilova)". If Becker is ranked higher, the routine will print
Martina Navratilova Boris Becker
If Navratilova is ranked higher, the routine will print
Boris Becker Martina Navratilova
But if they are equally ranked, the routine will print
Boris Becker Boris Becker
This is unlikely to be the intended output, hence the "gotcha". There would be no "gotcha" if 'min' returned 'current' and 'max' returned 'other' in the case of equal ranking, but that's not how 'min' and 'max' are specified.
Eiffel compilers differ on whether they allow two objects for which 'is_equal' returns false to nevertheless have equal sorting order from the point of view of COMPARABLE. In other words, whether "a < b or a > b or a.is_equal(b)" is ever allowed to be false. ETL suggests that it can be (by giving tennis rankings as an example - p475), yet the Eiffel Library Standard Vintage 95 clearly specifies that it can't be - by this postcondition to 'is_equal' in class COMPARABLE:
trichotomy: result = (not (current < other) and not (other < current))
The behaviour of 'min' and 'max' for comparably-equal 'current' and 'other' is also rigorously spelled out:
Here's the postcondition for 'min':
ensure
current_if_not_greater: (current <= other) implies (result = current)
other_if_greater: (current > other) implies (result = other)
and here's the postcondition for 'max':
ensure
current_if_not_smaller: (current >= other) implies (result = current)
other_if_smaller: (current < other) implies (result = other)
Eiffel and NICE are registered trademarks of the Nonprofit International Consortium for Eiffel.