Eiffel "Gocha" #3.B - Min and Max

Quote:

> 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 "Gocha" 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'.

Suppose we 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 "gocha". There would

be no "gocha" 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)

Regards,

Roger

--

--

-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525

-- Everything Eiffel: http://www.eiffel.demon.co.uk/ | +44-1772-687525