Browse Groups

• Here is an initial proposal for COMPARABLE. I think we can discuss this in one step, and vote on it in a block doing the different issues in separate votes,
Aug 6, 2002 1 of 9
View Source
Here is an initial proposal for COMPARABLE.

I think we can discuss this in one step, and vote on it
in a block doing the different issues in separate votes,
but at the same time or in rapid succession.

Points I see:

The name is misleading. What is modelled is a total
order. In mathematical terms "comparable" would
mean that there is an equality operator defined on a set,
not an order. Usually these exist and are total. The same
is true in Eiffel, look at feature "equal" to find it.

So COMPARABLE should really be named TOTALLY_ORDERED.
I am not proposing to change the name, but to change the

"Objects that may be compared according to a total order relation";
note: "The basic operation is `<` (less than); others are defined
in terms of this operation and `is_equal'."

I do not like the "may". It confuses things. My proposal:

"Objects of this type are ordered with respect to a total
order relation `<'. This basic operation is used together
with `is_equal' to define additional operators."

Furthermore I propose the following changes:

- Remove the invariant and put it in a postcondition
'strict' in '<'. Furthermore add a postcondition
'total' to '<'.
The advantage is that 'is_equal' need not be redefined
anymore as trichotomy is now defined in the contract of "<".
This is good as trichotomy is really a property of '<' that
is defined in relation to a given definition for 'is_equal'.
It is _not_ a constraint on 'is_equal'!

Affected: Features "<", 'is_equal'
Invariant 'irreflexive_comparison'

- 'min','max' are over-specified: When the elements are equal via
'is_equal' there is a preference for a specific result
(Current). The way I read the specification of 'is_equal' in
GENERAL is that a redefinition of 'is_equal' that has different
objects being equal is entirely permissible, as long as equality
implies same type and 'standard_is_equal' implies 'is_equal'. The
most general implementation would give 'is_equal' the same
semantics as 'same_type'.

I hope I got this right. Please correct me if not!

Change: Allow 'min', 'max' to return any argument
if arguments are equal via 'is_equal'.

Affected: Postconditions of features 'min', 'max'.

That seems to be it. If I missed something, please speak up!

Here is the rest of COMPARABLE from ELKS95. Places where I
think changes are needed are marked with '#' and a comment
behind it. The changes I propose are the following:

-----

feature -- Comparison
infix "<" (other: like Current): BOOLEAN
-- Is current object less than other?
require
other_exists: other /= Void
ensure
asymmetric: Result implies not (other < Current)
#
# strict: Result implies not Current.is_equal(other)
# total: not Current.is_equal(other) implies
# (Current < other or other < Current)
#
# This is in part covered by the invariant, but I feel it is needed
# here, and here only. I propose to remove the invariant.

infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal to other?
require
other_exists: other /= Void
ensure
definition: Result = (Current < other) or is_equal (other)

infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or equal to other?
require
other_exists: other /= Void
ensure
definition: Result = (other <= Current)
# Replace this with
#
# definition: Result = (other < Current) or is_equal (other)
#
# in order to get a direct dependency on the basic operations.

infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
require
other_exists: 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
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result;
trichotomy: Result = (not (Current < other) and not (other < Current))
#
# 'trichotomy' is redundant with the postcondition 'strict' on '<' and
# 'definition' on '>'. We could remove it and do without redefinition
# of 'is_equal' entirely. My personal feeling is that this would be the way
# to go: An order relation has to respect the already defined equality
# relation, _without_ putting any additional constraints on it.
# 'consistent' and 'symmetric' are already in GENERAL.
#

max (other: like Current): like Current
-- The greater of current object and other
require
other_exists: other /= Void
ensure
current_if_not_smaller: (Current >= other) implies (Result = Current)
other_if_smaller: (Current < other) implies (Result = other)
# This is too strict. If some objects change is_equal so that some
# different objects cannot be distinguished by 'is_equal' anymore
# this postcondition mandates that the result has to be 'Current'.
# There is no need for that.
# I would propose to replace the entire postcondition with
#
# definition: Result >= Current and Result >= other and
# (Result = Current or Result = other)
#
# neatly removing the problem.

min (other: like Current): like Current
-- The smaller of current object and other
require
other_exists: other /= Void
ensure
current_if_not_greater: (Current <= other) implies (Result = Current)
other_if_greater: (Current > other) implies (Result = other)
# Same thing as with 'max'. I propose to change the postcondition to
#
# definition: Result <= Current and Result <= other and
# (Result = Current or Result = other)
#

three_way_comparison (other: like Current): INTEGER)
-- If current object equal to other, 0; if smaller,
-- -1; if greater, 1.
require
other_exists: other /= Void
ensure
equal_zero: (Result = 0) = is_equal (other);
smaller_negative: (Result = -1) = (Current < other);
greater_positive: (Result = 1) = (Current > other)

invariant

irreflexive_comparison: not (Current < Current)
# I propose to remove this invariant. The postcondition 'strict' at
# feature '<' is entirely enough and is in the place where it belongs.

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
• ... Hmm, ugly: What about TOTALLY_ORDERABLE? it s deferred after all. (To non-methematicans COMPARE possibly means something like smaller or larger, maybe
Aug 6, 2002 1 of 9
View Source
On 6 Aug 2002, at 13:01, Arno Wagner wrote:

> Here is an initial proposal for COMPARABLE.
>
> I think we can discuss this in one step, and vote on it
> in a block doing the different issues in separate votes,
> but at the same time or in rapid succession.
>
> Points I see:
>
> The name is misleading. What is modelled is a total
> order. In mathematical terms "comparable" would
> mean that there is an equality operator defined on a set,
> not an order. Usually these exist and are total. The same
> is true in Eiffel, look at feature "equal" to find it.
>
> So COMPARABLE should really be named TOTALLY_ORDERED.

Hmm, ugly: What about TOTALLY_ORDERABLE? it's deferred after all.
(To non-methematicans COMPARE possibly means something like smaller or
larger, maybe that's why the original name was COMPARABLE).

> I am not proposing to change the name, but to change the
>
> "Objects that may be compared according to a total order relation";
> note: "The basic operation is `<` (less than); others are defined
> in terms of this operation and `is_equal'."

should "is_less_than" be declared as synonym for "<"? It would match
nicely with "is_equal"...

>
> I do not like the "may". It confuses things. My proposal:
>
> "Objects of this type are ordered with respect to a total
> order relation `<'. This basic operation is used together
> with `is_equal' to define additional operators."

Talking about objects of deferred classes is also not very good: What
about "Total order using `<' and `is_equal' as relational operators".
Is it too crisp?

>
> Furthermore I propose the following changes:
>
> - Remove the invariant and put it in a postcondition
> 'strict' in '<'. Furthermore add a postcondition
> 'total' to '<'.
> The advantage is that 'is_equal' need not be redefined
> anymore as trichotomy is now defined in the contract of "<".
> This is good as trichotomy is really a property of '<' that
> is defined in relation to a given definition for 'is_equal'.
> It is _not_ a constraint on 'is_equal'!

Maybe for the future: Quote the invariants and post conditions you are

>
> Affected: Features "<", 'is_equal'
> Invariant 'irreflexive_comparison'
>
> - 'min','max' are over-specified: When the elements are equal via
> 'is_equal' there is a preference for a specific result
> (Current). The way I read the specification of 'is_equal' in
> GENERAL is that a redefinition of 'is_equal' that has different
> objects being equal is entirely permissible, as long as equality
> implies same type and 'standard_is_equal' implies 'is_equal'. The
> most general implementation would give 'is_equal' the same
> semantics as 'same_type'.
>
> I hope I got this right. Please correct me if not!
>
> Change: Allow 'min', 'max' to return any argument
> if arguments are equal via 'is_equal'.
>
> Affected: Postconditions of features 'min', 'max'.
>
>
> That seems to be it. If I missed something, please speak up!
>
> Here is the rest of COMPARABLE from ELKS95. Places where I
> think changes are needed are marked with '#' and a comment
> behind it. The changes I propose are the following:
>
> -----
>
> feature -- Comparison
> infix "<" (other: like Current): BOOLEAN
> -- Is current object less than other?
> require
> other_exists: other /= Void
> ensure
> asymmetric: Result implies not (other < Current)
> #
> # strict: Result implies not Current.is_equal(other)

Maybe replace "strict" with "strict_ordering" (or similar).

> # total: not Current.is_equal(other) implies
> # (Current < other or other < Current)
> #

(same for "total")

> # This is in part covered by the invariant, but I feel it is needed
> # here, and here only. I propose to remove the invariant.
>
>
> infix "<=" (other: like Current): BOOLEAN
> -- Is current object less than or equal to other?
> require
> other_exists: other /= Void
> ensure
> definition: Result = (Current < other) or is_equal (other)
>
>
> infix ">=" (other: like Current): BOOLEAN
> -- Is current object greater than or equal to other?
> require
> other_exists: other /= Void
> ensure
> definition: Result = (other <= Current)
> # Replace this with
> #
> # definition: Result = (other < Current) or is_equal (other)
> #
> # in order to get a direct dependency on the basic operations.

>
>
> infix ">" (other: like Current): BOOLEAN
> -- Is current object greater than other?
> require
> other_exists: 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
> symmetric: Result implies other.is_equal (Current);
> consistent: standard_is_equal (other) implies Result;
> trichotomy: Result = (not (Current < other) and not (other < Current))

> #
> # 'trichotomy' is redundant with the postcondition 'strict' on '<' and
> # 'definition' on '>'. We could remove it and do without redefinition
> # of 'is_equal' entirely. My personal feeling is that this would be the way
> # to go: An order relation has to respect the already defined equality
> # relation, _without_ putting any additional constraints on it.
> # 'consistent' and 'symmetric' are already in GENERAL.
> #
>
>
>
> max (other: like Current): like Current
> -- The greater of current object and other
> require
> other_exists: other /= Void
> ensure
> current_if_not_smaller: (Current >= other) implies (Result = Current)
> other_if_smaller: (Current < other) implies (Result = other)
> # This is too strict. If some objects change is_equal so that some
> # different objects cannot be distinguished by 'is_equal' anymore
> # this postcondition mandates that the result has to be 'Current'.
> # There is no need for that.

Maybe if you use it implementing "stable sort algorithms" it could be
interesting.

> # I would propose to replace the entire postcondition with
> #
> # definition: Result >= Current and Result >= other and
> # (Result = Current or Result = other)
> #
> # neatly removing the problem.
>
>
>
> min (other: like Current): like Current
> -- The smaller of current object and other
> require
> other_exists: other /= Void
> ensure
> current_if_not_greater: (Current <= other) implies (Result = Current)
> other_if_greater: (Current > other) implies (Result = other)
> # Same thing as with 'max'. I propose to change the postcondition to
> #
> # definition: Result <= Current and Result <= other and
> # (Result = Current or Result = other)
> #
>
>
> three_way_comparison (other: like Current): INTEGER)
> -- If current object equal to other, 0; if smaller,
> -- -1; if greater, 1.
> require
> other_exists: other /= Void
> ensure
> equal_zero: (Result = 0) = is_equal (other);
> smaller_negative: (Result = -1) = (Current < other);
> greater_positive: (Result = 1) = (Current > other)

Hmm.

zero_if_equal: is_equal(other) implies Result = 0
negative_if_smaller: Current < other implies Result = -1
positive_if_larger: Current > other implies Result = 1

??? What about that the left sides should have empty intersections

>
> invariant
>
> irreflexive_comparison: not (Current < Current)
> # I propose to remove this invariant. The postcondition 'strict' at
> # feature '<' is entirely enough and is in the place where it belongs.
>
> end
>

Regards,
Ulrich
• Hi all ! ... Why not : current_or_other: Result = Current or Result = other at_least_current: Result = Current at_least_other: Result = other Isn t it better
Aug 6, 2002 1 of 9
View Source
Hi all !

On Tuesday 06 August 2002 13:01, Arno Wagner wrote:
>
> max (other: like Current): like Current
> -- The greater of current object and other
> require
> other_exists: other /= Void
> ensure
> current_if_not_smaller: (Current >= other) implies (Result =
> Current) other_if_smaller: (Current < other) implies (Result = other) #
> This is too strict. If some objects change is_equal so that some #
> different objects cannot be distinguished by 'is_equal' anymore
> # this postcondition mandates that the result has to be 'Current'.
> # There is no need for that.
> # I would propose to replace the entire postcondition with
> #
> # definition: Result >= Current and Result >= other and
> # (Result = Current or Result = other)
> #
> # neatly removing the problem.

Why not :

current_or_other: Result = Current or Result = other
at_least_current: Result >= Current
at_least_other: Result >= other

Isn't it better when the conditions are splited as mus as possible ?

> min (other: like Current): like Current
> -- The smaller of current object and other
> require
> other_exists: other /= Void
> ensure
> current_if_not_greater: (Current <= other) implies (Result =
> Current) other_if_greater: (Current > other) implies (Result = other) #
> Same thing as with 'max'. I propose to change the postcondition to #
> # definition: Result <= Current and Result <= other and
> # (Result = Current or Result = other)
> #

As above :

current_or_other: Result = Current or Result = other
at_most_current: Result <= Current
at_most_other: Result <= other

Regards,
Christian.
• ... Indeed. I like this proposal. [ same for min spipped] Rgerads, Arno -- Arno Wagner, Communication Systems Group, ETH Zuerich, wagner@tik.ee.ethz.ch
Aug 6, 2002 1 of 9
View Source
On Tue, Aug 06, 2002 at 08:28:46PM +0200, Christian Couder wrote:
> Hi all !
>
> On Tuesday 06 August 2002 13:01, Arno Wagner wrote:
> >
> > max (other: like Current): like Current
> > -- The greater of current object and other
> > require
> > other_exists: other /= Void
> > ensure
> > current_if_not_smaller: (Current >= other) implies (Result =
> > Current) other_if_smaller: (Current < other) implies (Result = other) #
> > This is too strict. If some objects change is_equal so that some #
> > different objects cannot be distinguished by 'is_equal' anymore
> > # this postcondition mandates that the result has to be 'Current'.
> > # There is no need for that.
> > # I would propose to replace the entire postcondition with
> > #
> > # definition: Result >= Current and Result >= other and
> > # (Result = Current or Result = other)
> > #
> > # neatly removing the problem.
>
> Why not :
>
> current_or_other: Result = Current or Result = other
> at_least_current: Result >= Current
> at_least_other: Result >= other
>
> Isn't it better when the conditions are splited as mus as possible ?

Indeed. I like this proposal.

[ same for 'min' spipped]

Arno

--
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
• ... Cannot it be simplified to # strict: Result implies not is_equal (other) # total: not is_equal (other) implies # (Result or
Aug 7, 2002 1 of 9
View Source
Arno Wagner wrote:

> feature -- Comparison
> infix "<" (other: like Current): BOOLEAN
> -- Is current object less than other?
> require
> other_exists: other /= Void
> ensure
> asymmetric: Result implies not (other < Current)
> #
> # strict: Result implies not Current.is_equal(other)
> # total: not Current.is_equal(other) implies
> # (Current < other or other < Current)
> #
> # This is in part covered by the invariant, but I feel it is needed
> # here, and here only. I propose to remove the invariant.

Cannot it be simplified to

# strict: Result implies not is_equal (other)
# total: not is_equal (other) implies
# (Result or other < Current)

?

> infix "<=" (other: like Current): BOOLEAN
> -- Is current object less than or equal to other?
> require
> other_exists: other /= Void
> ensure
> definition: Result = (Current < other) or is_equal (other)

Should not it be

definition: Result = ((Current < other) or is_equal (other))

?

> infix ">=" (other: like Current): BOOLEAN
> -- Is current object greater than or equal to other?
> require
> other_exists: other /= Void
> ensure
> definition: Result = (other <= Current)
> # Replace this with
> #
> # definition: Result = (other < Current) or is_equal (other)
> #
> # in order to get a direct dependency on the basic operations.

The same here.

Regards,
Alexander Kogtenkov
Object Tools, Moscow
• ... It makes sure that the expression is considered properly. Without parentheses it would be interpreted as trichotomy: (Result = not (Current
Aug 7, 2002 1 of 9
View Source
Ulrich Windl wrote:

> > 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
> > symmetric: Result implies other.is_equal (Current);
> > consistent: standard_is_equal (other) implies Result;
> > trichotomy: Result = (not (Current < other) and not (other < Current))
>

It makes sure that the expression is considered properly.
Without parentheses it would be interpreted as

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

Regards,
Alexander Kogtenkov
Object Tools, Moscow
• ... Yes it can. I don t mind either way. The first is more explicit, the second one more compact. Both do the job. ... Indeed. I keep forgetting that. Regards,
Aug 7, 2002 1 of 9
View Source
On Wed, Aug 07, 2002 at 01:46:34PM +0400, Alexander Kogtenkov wrote:
> Arno Wagner wrote:
>
> > feature -- Comparison
> > infix "<" (other: like Current): BOOLEAN
> > -- Is current object less than other?
> > require
> > other_exists: other /= Void
> > ensure
> > asymmetric: Result implies not (other < Current)
> > # Add the following:
> > #
> > # strict: Result implies not Current.is_equal(other)
> > # total: not Current.is_equal(other) implies
> > # (Current < other or other < Current)
> > #
> > # This is in part covered by the invariant, but I feel it is needed
> > # here, and here only. I propose to remove the invariant.
>
> Cannot it be simplified to
>
> # strict: Result implies not is_equal (other)
> # total: not is_equal (other) implies
> # (Result or other < Current)
>
> ?

Yes it can. I don't mind either way. The first is
more explicit, the second one more compact. Both
do the job.

> > infix "<=" (other: like Current): BOOLEAN
> > -- Is current object less than or equal to other?
> > require
> > other_exists: other /= Void
> > ensure
> > definition: Result = (Current < other) or is_equal (other)
>
> Should not it be
>
> definition: Result = ((Current < other) or is_equal (other))
>
> ?

Indeed. I keep forgetting that.

Regards,
Arno

--
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
• Hey Arno, Thanks for taking the lead, both for the group in general and for COMPARABLE in particular. I m sure you ll do a great job! More below. ... I like
Aug 9, 2002 1 of 9
View Source
Hey Arno,

Thanks for taking the lead, both for the group in
general and for COMPARABLE in particular. I'm sure
you'll do a great job!

More below.

Arno Wagner wrote:

>
> Here is an initial proposal for COMPARABLE.
>
> I think we can discuss this in one step, and vote on it
> in a block doing the different issues in separate votes,
> but at the same time or in rapid succession.
>
> Points I see:
>
> The name is misleading. What is modelled is a total
> order. In mathematical terms "comparable" would
> mean that there is an equality operator defined on a set,
> not an order. Usually these exist and are total. The same
> is true in Eiffel, look at feature "equal" to find it.
>
> So COMPARABLE should really be named TOTALLY_ORDERED.
> I am not proposing to change the name, but to change the
>
> "Objects that may be compared according to a total order relation";
> note: "The basic operation is `<` (less than); others are defined
> in terms of this operation and `is_equal'."
>
> I do not like the "may". It confuses things. My proposal:
>
> "Objects of this type are ordered with respect to a total
> order relation `<'. This basic operation is used together
> with `is_equal' to define additional operators."

I like this change, but note that actually we can do it
entirely in terms of `<' as the basic specifier for
COMPARABLE.

>
> Furthermore I propose the following changes:
>
> - Remove the invariant and put it in a postcondition
> 'strict' in '<'. Furthermore add a postcondition
> 'total' to '<'.
> The advantage is that 'is_equal' need not be redefined
> anymore as trichotomy is now defined in the contract of "<".
> This is good as trichotomy is really a property of '<' that
> is defined in relation to a given definition for 'is_equal'.
> It is _not_ a constraint on 'is_equal'!
>
> Affected: Features "<", 'is_equal'
> Invariant 'irreflexive_comparison'

I see the point, but I disagree. 'is_equal' will have
to be redefined anyway in all but trivial cases as
exemplified by STRING and ARRAY. Might as well be up
front about it. Besides the whole idea of the disciplined
approach we're using is to identify a few (in this
case one) basic specifiers and define everything else
in terms of them. Ideally the basic specifiers themselves
have no postconditions.

So I'd prefer this back the other way. It may well
be, however, that 'trichotomy' is not the best label
for the clause in the postcondition of 'is_equal'.

The deeper and harder problem here is whether 'is_equal'
is the right version of equality to play a role in
in the total ordering. Those extra postconditions make
this somewhat problematic. If is_equal returns False
only because of type mismatch, which of < and > will
be true?

>
> - 'min','max' are over-specified: When the elements are equal via
> 'is_equal' there is a preference for a specific result
> (Current). The way I read the specification of 'is_equal' in
> GENERAL is that a redefinition of 'is_equal' that has different
> objects being equal is entirely permissible, as long as equality
> implies same type and 'standard_is_equal' implies 'is_equal'. The
> most general implementation would give 'is_equal' the same
> semantics as 'same_type'.
>
> I hope I got this right. Please correct me if not!
>
> Change: Allow 'min', 'max' to return any argument
> if arguments are equal via 'is_equal'.
>
> Affected: Postconditions of features 'min', 'max'.

Interesting. I don't have any problem letting the implementer
decide which of Current or other to return. Although if
we do that I think we should somehow mark the spec as
indeterminate in this case.

But I'm not sure of the reasoning. If 'is_equal' is
redefined to mean 'same_type' (or any other redefinition)
why would you then prefer to return 'other' as the max?.
Perhaps an example would help?

>
>
> That seems to be it. If I missed something, please speak up!
>
> Here is the rest of COMPARABLE from ELKS95. Places where I
> think changes are needed are marked with '#' and a comment
> behind it. The changes I propose are the following:

Nice job putting all this together! Still more below.

>
> -----
>
> feature -- Comparison
> infix "<" (other: like Current): BOOLEAN
> -- Is current object less than other?
> require
> other_exists: other /= Void
> ensure
> asymmetric: Result implies not (other < Current)
> #
> # strict: Result implies not Current.is_equal(other)
> # total: not Current.is_equal(other) implies
> # (Current < other or other < Current)
> #
> # This is in part covered by the invariant, but I feel it is needed
> # here, and here only. I propose to remove the invariant.

As noted above, I'd put this back the way it was before, no
postconditions.

>
>
> infix "<=" (other: like Current): BOOLEAN
> -- Is current object less than or equal to other?
> require
> other_exists: other /= Void
> ensure
> definition: Result = (Current < other) or is_equal (other)

I'd prefer Result = not (other < Current)

Keep every definition strictly in terms of <. Well at
least all the simple ones. We may have to vary from
this when we hit max, min, three_way.

>
>
> infix ">=" (other: like Current): BOOLEAN
> -- Is current object greater than or equal to other?
> require
> other_exists: other /= Void
> ensure
> definition: Result = (other <= Current)
> # Replace this with
> #
> # definition: Result = (other < Current) or is_equal (other)
> #
> # in order to get a direct dependency on the basic operations.

Result = not (Current < other)

>
>
> infix ">" (other: like Current): BOOLEAN
> -- Is current object greater than other?
> require
> other_exists: other /= Void
> ensure
> definition: Result = (other < Current)

Good.

>
>
> 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
> symmetric: Result implies other.is_equal (Current);
> consistent: standard_is_equal (other) implies Result;
> trichotomy: Result = (not (Current < other) and not (other < Current))
> #
> # 'trichotomy' is redundant with the postcondition 'strict' on '<' and
> # 'definition' on '>'. We could remove it and do without redefinition
> # of 'is_equal' entirely. My personal feeling is that this would be the way
> # to go: An order relation has to respect the already defined equality
> # relation, _without_ putting any additional constraints on it.
> # 'consistent' and 'symmetric' are already in GENERAL.
> #

Again, I would keep this as it was, see above for reasoning.
'definition' might be a better name than 'trichotomy'.

>
>
>
> max (other: like Current): like Current
> -- The greater of current object and other
> require
> other_exists: other /= Void
> ensure
> current_if_not_smaller: (Current >= other) implies (Result = Current)

Hmmm... Could be not (Current < other) implies (Result = Current)

> other_if_smaller: (Current < other) implies (Result = other)
> # This is too strict. If some objects change is_equal so that some
> # different objects cannot be distinguished by 'is_equal' anymore
> # this postcondition mandates that the result has to be 'Current'.
> # There is no need for that.
> # I would propose to replace the entire postcondition with
> #
> # definition: Result >= Current and Result >= other and
> # (Result = Current or Result = other)
> #
> # neatly removing the problem.

No objection in principle, but again I'm not sure it's a useful
change....

>
>
>
> min (other: like Current): like Current
> -- The smaller of current object and other
> require
> other_exists: other /= Void
> ensure
> current_if_not_greater: (Current <= other) implies (Result = Current)
> other_if_greater: (Current > other) implies (Result = other)

(other < Current) implies....

> # Same thing as with 'max'. I propose to change the postcondition to
> #
> # definition: Result <= Current and Result <= other and
> # (Result = Current or Result = other)
> #

Ditto.

>
>
> three_way_comparison (other: like Current): INTEGER)
> -- If current object equal to other, 0; if smaller,
> -- -1; if greater, 1.
> require
> other_exists: other /= Void
> ensure
> equal_zero: (Result = 0) = is_equal (other);
> smaller_negative: (Result = -1) = (Current < other);
> greater_positive: (Result = 1) = (Current > other)

For the last one perhaps (Result = 1) = (other < Current)

That way _everything_ is defined in terms of < except the
one clause equal_zero immediately above. And I don't see
a way to fix that one without really damaging readability.

>
> invariant
>
> irreflexive_comparison: not (Current < Current)
> # I propose to remove this invariant. The postcondition 'strict' at
> # feature '<' is entirely enough and is in the place where it belongs.

Well, most invariants are redundant. Again see STRING and ARRAY. The
idea is to provide summary information to confirm the abstraction,
in this case a total ordering. I'd actually like to see more. E.g.

reflexive_comparison: Current <= Current (there's probably a
better name.)

-- asymmetry: for_all other : like Current
-- ((other < Current) implies not (Current < other))

-- antisymmetry: for_all other : like Current
-- ((other <= Current) and (Current <= other) implies is_equal(other))

-- trichotomy: for_all other : like Current
-- ((other < Current) or (Current < other) or is_equal(other))

Again there may be better names. Indeed to get full trichotomy
you'd need to specify that just one of the three is true.
And they're not compilable, but again they confirm the fact that
we're really specifying a total ordering.

Arno, Michael Schweitzer and Bertrand did some work a few years
back that included variations of COMPARABLE such as partial ordering.
Does it make any sense for me to dig that out, or is it enough
to just work on COMPARABLE for the time being?

Hope this helps,
-- Jim

>
> 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
>
>
> ---------------------------
>
> http://www.eiffel-nice.org/
>
> --------------------------
>
> Your use of Yahoo! Groups is subject to http://docs.yahoo.com/info/terms/
>
>
>
• ... Thanks for the confidence! I ll do my best. I am sure it will be a learning experience though. As for your comments, I might post a detailed answer in the
Aug 9, 2002 1 of 9
View Source
On Fri, Aug 09, 2002 at 12:01:39PM -0400, James McKim wrote:
> Hey Arno,
>
> Thanks for taking the lead, both for the group in
> general and for COMPARABLE in particular. I'm sure
> you'll do a great job!

Thanks for the confidence! I'll do my best.
I am sure it will be a learning experience though.

in the next days, but I have a wacky idea now:

[...]
> I like this change, but note that actually we can do it
> entirely in terms of `<' as the basic specifier for
> COMPARABLE.
[...]

We can, but it has some interesting consequences. If
we do a total order in terms of `<' only, that means
that equality will be defined in terms of `<' only.
(Equality is needed because of totality unless we
allow only `='-equality.)
Let `===' denote this type of "equality with respect
to `<'" for the moment.

The definition for `===' would be

for all a,b:
a === b if and only if ( not(a<b) and not(b<a) )

neatly enforcing totality of `<'. (Although probably
not quite in the way people expect. `===' would
be kind of a kernel relation here.) Without `==='
the problem would be that not(a<b) and not(b<a)
could be true, while a and b are not the same
object. This would make `<' partial.

If we spin this a little further, we can indeed use
the above definition of "equality with respect to `<'"
and define all the other operators according to it.

`>',`<=',`>=' are no problem. `===' is not even needed here.

max(a,b):
if a>b then max(a,b) = a
if b>a then max(a,b) = b
if a===b then max(a,b) = a or max(a,b) = b

`min' analog.

`three_way_comparison' analog.

Added benefit: `is_equal' does not make an appearence
in this at all! `===' and `is_equal' are completely
independent. Getting rid of the forced relation between
`===' and `is_equal' _would_ be nice in mu opinion.
(Everybody that wants this relation can still define
`<' accordingly.)

The one problem I see is what to do with `==='?

- First option: Redefine `is_equal' to
have the semantics of `==='. That is how it was done
up to now. Problem: `is_equal' is sort of a 'higher'
concept than `<'. To me it feels wrong to change the
basic notion of equality in order to accomodate the
less basic notion of order.

- Second option: Have a new explicit operator `==='
(naming to be determined). Would this operator really
offer an added benefit or just clutter the interface?
Personally I might prefer this one.

- Third option: Do not have an explicit `===' operator.
It is not a good idea to have a defined notion
for equality (`===') but no explicit name/operator for it,
so this is probably not be the way to go.

- Fourth option: Have `===' defined as `is_equal'
and constrain `<' accordingly. This would make sense
insofar as `is_equal' is meta-equality in Eiffel. On the
other hand we might just want a special kind of equality
with regard to order and constraining `<' is indeed not
elegant. (This was my original proposal.)

- Fifth option: Define `===' as `='. This seems very
constraining. On the other hand, is this not what we are
thinking of when we say "ordered"? Mathematically it is.

This option has one strong benefit: It ensures
that objects can always be sorted/orderd in one way only.
Of two different opjects one will always be larger.
In a sense all the other options above are only there
because we allow an equivalence relation (`is_equal') to
take the place of equality, but at the same time cannot do
a complete factoring, i.e. things that are equal via
`is_equal' can still be distinguished.

- Other ideas ??

This totality requirement has indeed some interesting
consequences....

Regards,
Arno

P.S.: I don't think a discussion about partial orders will
help us much. There are many types of these and often you
actually want a lattice, making things even more general
and the number of variants very, very large. So unless you
have this papers handy, don't bother.

---
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
Your message has been successfully submitted and would be delivered to recipients shortly.
• Changes have not been saved
Press OK to abandon changes or Cancel to continue editing
• Your browser is not supported
Kindly note that Groups does not support 7.0 or earlier versions of Internet Explorer. We recommend upgrading to the latest Internet Explorer, Google Chrome, or Firefox. If you are using IE 9 or later, make sure you turn off Compatibility View.