- Eric Bezault wrote:

> Sorry for not reviewing class COMPARABLE before. You know what

Yes, same here. The last 3 weeks where crazy (start of the

> it is: lack of time, etc.

lectures and the flu going round).

As to Eric's comments:

O.K., I have corrected the header and replaced all the

"other_exists" with "other_not_void".

I am not aware of the status on ANY vs. ANY/GENERAL. Does

anybody know what it is and can give me a pointer?

As to "same_type: Result implies same_type (other)" for

"is_equal". O.k. I have added that, although it is completely

redundant. There is what I fear is a serious bug in Eiffel.

It manifests itself in the postcondition "symmetric" of

"is_equal" actually specifying a run-time type constraint.

If you call "is_equal" with something of not "same_type"

you get a run-time type violation. Very bad.

This might also be the reason why at least SE does not

have the postcondition "symmetric" on "is_equal".

I think it was while thinking about this that I threw

out the postcondition 'same_type'....

I am not quite sure about the way to tackle this, but

it is obviously not what was intended by feature "is_equal".

As I suspect all the vendors for now ignore the postcondition

"symmetric", I propose to just live with the problem for now

and add "revision of ANY/General" to the end of the TODO-list.

The changes made there should then propagate automatically

to all the classes redefining 'is_equal'. However if there

is a desire to tackle this problem now, we can also make it

the next topic.

for "max":> > max (other: like Current): like Current

Indeed. So the "at_least..." postconditions will have to

> > -- The greater of current object and other, implementers choice

> > -- if they are equal

> > require

> > other_exists: other /= Void

> > ensure

> > current_or_other: (Result = Current) or (Result = other)

> > at_least_current: (Result = Current) or (Current < Result)

> > at_least_other: (Result = other) or (other < Result)

>

> Consider that:

>

> other /= Current

> other.is_equal (Current)

>

> Therefore Result is either 'other' or 'Current' (implementers choice).

> Consider that it's 'Current'. The postcondition 'at_least_other' says

> that 'other < Result' (because 'Result /= other'). But 'Result = Current',

> so we have 'other < Current'. This violates our assumption that

> 'other.is_equal (Current)'. Or did a miss something?

change. Ulrich proposed

current_or_other: (Result = Current) or (Result = other)

result_is_other: Current < other implies Result = other

result_is_current: other < Current implies Result = Current

which I like and have added.

For the indention of the invariant, I do not really care.

I have attempted some beautification, but if anybody sees

a better way, please tell me.

As for looking at STRING now, I would propose to deferr that to

the next iteration. Since the functionality here does not change

(or gets more general in the case of three_way_comparison), I

expect there will be no problems.

Comments? Questions? Proposals?

Arno

----------------------------------------------------------------------

indexing

description: "Objects of this type are ordered with respect %

%to a total order relation."

Note: "The basic operation `<' is is used to define all other %

%operations. `is_equal' is redefined in terms of `<'."

deferred class interface

feature -- Basic Specifiers

infix "<" (other: like Current): BOOLEAN

-- Is current object less than other?

require

other_not_void: other /= Void

feature -- Comparison

infix "<=" (other: like Current): BOOLEAN

-- Is current object less than or equal to `other'?

require

other_not_void: other /= Void

ensure

definition: Result = not (other < Current)

infix ">=" (other: like Current): BOOLEAN

-- Is current object greater than or equal to `other'?

require

other_not_void: other /= Void

ensure

definition: Result = not (Current < other)

infix ">" (other: like Current): BOOLEAN

-- Is current object greater than `other'?

require

other_not_void: other /= Void

ensure

definition: Result = (other < Current)

is_equal (other: like Current): BOOLEAN

-- Is `other' attached to an object considered equal

-- to current object?

-- (Redefined from GENERAL.)

require

other_not_void: other /= Void

ensure

definition: Result = (not (Current < other) and

not (other < Current))

symmetric: Result implies other.is_equal (Current);

consistent: standard_is_equal (other) implies Result;

same_type: Result implies same_type (other)

three_way_comparison (other: like Current): INTEGER)

-- If current object equal to `other', 0; if smaller,

-- -1; if greater, 1.

-- Redundant postcondition included for clarity.

require

other_not_void: other /= Void

ensure

legal_result: Result = -1 or Result = 0 or Result = 1

zero_on_equal: (Result = 0) =

(not (Current < other) and not (other < Current))

positive_on_larger: (Result = 1) = (other < Current)

negative_on_smaller: (Result = -1) = (Current < other)

feature -- Selection

max (other: like Current): like Current

-- The greater of current object and `other', implementers choice

-- if they are equal.

require

other_not_void: other /= Void

ensure

current_or_other: (Result = Current) or (Result = other)

result_is_other: Current < other implies Result = other

result_is_current: other < Current implies Result = Current

min (other: like Current): like Current

-- The smaller of current object and `other', implementers choice

-- if they are equal.

require

other_not_void: other /= Void

ensure

current_or_other: (Result = Current) or (Result = other)

result_is_other: other < Current implies Result = other

result_is_current: Current < other implies Result = Current

invariant

irreflexivity: not (Current < Current)

-- asymmetry: for_all other : like Current :

-- ((other < Current) implies not (Current < other))

-- transitivity: for_all second : like Current :

-- for all third : like Current :

-- ((second < Current) and (Current < third) implies (second < third)

-- trichotomy: for_all other : like Current :

-- exactly_one_of(other < Current, Current < other, is_equal(other))

end

--

Arno Wagner, Communication Systems Group, ETH Zuerich, wagner@...

GnuPG: ID: 1E25338F FP: 0C30 5782 9D93 F785 E79C 0296 797F 6B50 1E25 338F

----

For every complex problem there is an answer that is clear, simple,

and wrong. -- H L Mencken - Arno Wagner wrote:
>

-------------------------------------^^^^^^

> indexing

>

> description: "Objects of this type are ordered with respect %

> %to a total order relation."

> Note: "The basic operation `<' is is used to define all other %

Two 'is'.

> %operations. `is_equal' is redefined in terms of `<'."

The class name is missing here.

>

> deferred class interface

>

> feature -- Basic Specifiers

--

Eric Bezault

mailto:ericb@...

http://www.gobosoft.com

___________________________________________________________________

Haut D�bit: Modem offert soit 150,92 euros rembours�s sur le Pack eXtense de Wanadoo !

Profitez du Haut D�bit � partir de 30 euros/mois : http://www.ifrance.com/_reloc/w