NICE-ESG-Libs Digest Thu, 23 Feb 95 Volume 1 : Issue 190
Today's Topics:
LIB95-PAJ-COMPARABLE
LIB95-PAJ-PART_COMPARABLE
NICE Eiffel Standards Group -- Library Committee Mailing List
To post to list:
NICE-ESG-Libs@atlanta.twr.com
To send mail to the Chairman of the committee:
NICE-ESG-Libs-chair@atlanta.twr.com
Administrative matters (sign up, unsubscribe, mail problems, etc):
NICE-ESG-Libs-request@atlanta.twr.com
Date: Fri, 24 Feb 1995 11:07:52 +1100 (EST)
From: cmingins@apple.fcit.monash.edu.au (Christine Mingins)
Subject: LIB95-PAJ-COMPARABLE
To: nice-esg-libs@atlanta.twr.com
LIB95-PAJ-COMPARABLE
--------------------
SUMMARY:
--------
This is a companion motion to LIB95-PAJ-PART_COMPARABLE. It describes
how the proposed changes to PART_COMPARABLE will affect the version of
COMPARABLE defined in LIB95-TWR-COMPARABLE.
1: The "order_equal" routine inherited from PART_COMPARABLE is
effected, and its postconditions strengthened.
2: The "<" routine is redefined to strengthen its postconditions. It
is still left deferred.
3: "max" now returns "Current" if "Current.order_equal (other)".
RATIONALE:
----------
1: Given two COMPARABLE objects a and b, exactly one of "a < b",
"a.order_equal (b)" and "b < a" must be true. This is a stronger
condition than for PART_COMPARABLE (where at most one of them may
be true), and this is reflected in the stronger postconditions.
2: Given a definition of "<", order equality can be defined as "not a
< b and not b < a". Descendants of COMPARABLE are of course free
to redefine this routine in a more efficient way.
3: The routines `min' and `max' both take an argument `other'. If
`Current' equals `other' then the Tower proposal had `min' return
`Current' and `max' return `other'. Hence if `a' and `b' were
equal then
a.min(b) = b.max(a)
This is counter-intuitive and hard to remember. Hence this
proposal defines both routines as returning `Current' if
`Current.order_equal (other)'.
Given two objects `a' and `b' to be split into `larger' and `smaller',
we can still ensure that `larger /= smaller' by writing
smaller = a.min(b);
larger = b.max(a);
Furthermore this makes explicit the decision about which of `a' and
`b' will be considered as smaller when they are order_equal.
SHORT:
------
-----------------------------------------------------------------------------
-- Elements that may be compared for a totral order relation.
-- Descendants need only define the behaviour of `infix "<"'.
deferred class interface COMPARABLE
feature summary
order_equal (other: like Current) : BOOLEAN
infix "<" (other: like Current) : BOOLEAN
infix "<=" (other: like Current) : BOOLEAN
infix ">" (other: like Current) : BOOLEAN
infix ">=" (other: like Current) : BOOLEAN
max (other: like Current): like Current
min (other: like Current): like Current
three_way_comparison (other: like Current): INTEGER
inherit
PART_COMPARABLE
redefine infix ">", order_equal
feature specification
-- Features redefined from PART_COMPARABLE
order_equal (other: like Current) : BOOLEAN
-- Is `Current' at the same place in the ordering as `other'?
require
other_not_void: other /= Void;
ensure
commutive: Result = (other.order_equal (Current));
definition: Result = (not Current < other and
not other < Current);
reference_equal: (Current = other) implies Result;
infix "<" (other: like Current) : BOOLEAN
-- Is `Current' strictly less than `other'?
require
other_not_void: other /= Void;
deferred
ensure
consistent: Result = (not Current.order_equal (other) and
not other < Current);
feature specification
-- Effective routines whose behaviour are determined by the
-- behaviour of `order_equal' and `infix "<"'.
--
-- Inherited from PART_COMPARABLE
infix "<=" (other: like Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void: other /= Void;
ensure
definition: Result = (Current.order_equal (other) or
Current < other);
infix ">" (other: like Current) : BOOLEAN
-- Is `Current' strictly greater than `other'?
require
other_not_void: other /= Void;
ensure
definition: Result = (other < Current);
infix ">=" (other: like Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void: other /= Void;
ensure
definition: Result = (other <= Current);
feature specification
-- Other useful features for comparable objects.
three_way_comparison (other: like Current): INTEGER
-- The relative position of `Current' and `other':
-- `< 0' if `Current < other';
-- `= 0' if `Current = other';
-- `> 0' if `Current > other';
require
other_not_void: other /= Void;
ensure
equal_zero: (Result = 0) = Current.order_equal (other);
smaller_negative: (Result < 0) = (Current < other);
greater_positive: (Result > 0) = (Current > other);
min (other: like Current) : like Current
-- The smaller of `Current' and `other'. Returns `Current'
-- if they are equal.
require
other_not_void: other /= Void;
ensure
not_void: Result /= Void;
current_if_not_greater: (Current <= other) implies (Result = Current);
otherwise_other: (Current > other) implies (Result = other);
max (other: like Current) : like Current
-- The larger of `Current' and `other'. Returns `Current'
-- if they are equal.
require
other_not_void: other /= Void;
ensure
not_void: Result /= Void;
current_if_not_smaller: (Current >= other) implies (Result = Current);
otherwise_other: (Current < other) implies (Result = other);
end interface -- class COMPARABLE
--
Paul Johnson | GEC-Marconi Ltd is not responsible for my opinions. |
+44 245 473331 ext 3245 +-----------+-----------------------------------------+
Work: | You are lost in a twisty maze of little
Home: | standards, all different.
Date: Fri, 24 Feb 1995 11:09:40 +1100 (EST)
From: cmingins@apple.fcit.monash.edu.au (Christine Mingins)
Subject: LIB95-PAJ-PART_COMPARABLE
To: nice-esg-libs@atlanta.twr.com
LIB95-PAJ-PART_COMPARABLE
-------------------------
SUMMARY:
--------
The following proposal is a modification to
LIB-95-TWR-PART_COMPARABLE.
1: A new deferred routine: "order_equal" is introduced to
PART_COMPARABLE (and hence inherited by COMPARABLE).
2: The operator "<=" is defined in terms of "<" and "order_equal".
3: Postconditions for "<" and "<=" are modified to refer to
"order_equal".
4: Order equality is now implied by shallow equality rather than
reference equality.
RATIONALE:
----------
1: "order_equal" is a natural addition to the PART_COMPARABLE class.
At most one of "a < b", "a.order_equal (b)" and "b < a" may be
true.
2: PART_COMPARABLE should define one of the operations "<", "<=" and
"order_equal" in terms of the other two. LIB95-TWR-PART_COMPARABLE
notes that many abstract maths texts define order equality in terms
of "<" and "<=", and so leaves these two deferred. The
"three_way_comparison" operator in COMPARABLE provides an
order_equality test defined in terms of "<" and "<=".
In most (if not all) cases, the definition of "<=" will be more
complex than the definition of "=". For example, consider a
COMPARABLE class where instances are ordered by two integer
features "a" and "b". The "b" value is significant only if the "a"
values are equal. Hence if we are comparing "Current" and "other",
the "<" operation can be defined as
if a = other.a then
Result := (b < other.b);
else
Result := (a < other.a);
end;
"order_equal" as
Result := (a = other.a) and (b = other.b);
and "<=" as
if a = other.a then
Result := (b <= other.b);
else
Result := (a < other.a);
end;
It is obvious that the "order_equal" is the simplest definition of
the three, and I would argue that the "<=" definition is the most
complicated and error-prone thanks to the varying use of "<" and
"<=" in different lines. In addition I believe that most software
engineers would intuitively consider "<=" to be an operator derived
from "<" and "=", whatever the mathematicians say. Hence I propose
that "<=" be defined in terms of "<" and "order_equal".
3: An earlier posting suggested that a new infix operator be defined
instead of "order_equal". This proposal does not include such an
operator because:
* The priority of "free" operators is not the same as other
comparison operators. Hence such an operator would be a subtle
source of bugs.
* Eiffel programmers are accustomed to thinking in of infix "=" as
a reference operator and "equal" as shallow equality. Since
order equality is conceptually similar to shallow equality, the
alphabetic term should be used.
4: Together the new postconditions on "<", "<=" and "order_equal"
define the important properties, in particular the consistency
property that at most one of "a < b", "a.order_equal(b)" and "b <
a" can be true.
5: Order equality is implied by reference equality but not shallow
equality. It may seem that if two objects have the same contents
then they should be in the same position in any partial or total
ordering. However it is possible to construct examples where two
objects can be shallow equal without being order equal (for
example, two nodes in a DAG with identical contents but different
parents).
SHORT:
------
----------------------------------------------------------------------------
-- Elements that may be compared in a partial order relation. If the
-- elements being compared are not comparable with one another then
-- these features return `False'. Note that order equality is not
-- necessarily the same as `is_equal', since `is_equal' is not
-- necessarily tied to the notion of ordering. Therefore the partial
-- ordering is defined in terms of the deferred features, `infix "<"'
-- and `order_equal'.
deferred class interface PART_COMPARABLE
feature summary
order_equal (other: like Current) : BOOLEAN
infix "<" (other: like Current) : BOOLEAN
infix "<=" (other: like Current) : BOOLEAN
infix ">" (other: like Current) : BOOLEAN
infix ">=" (other: like Current) : BOOLEAN
feature specification
-- Deferred routines that determine the partial ordering
order_equal (other: like Current) : BOOLEAN
-- Is `Current' at the same place in the ordering as `other'?
require
other_not_void: other /= Void;
deferred
ensure
commutive: Result = (other.order_equal (Current));
consistent: Result implies (not Current < other and
not other < Current);
reference_equal: Current = other implies Result;
infix "<" (other: like Current) : BOOLEAN
-- Is `Current' strictly less than `other'?
require
other_not_void: other /= Void;
deferred
ensure
consistent: Result implies (not Current.order_equal (other) and
not other < Current);
feature specification
-- Effective routines whose behaviour are determined by the
-- behaviour of `order_equal' and `infix "<"'.
infix "<=" (other: like Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void: other /= Void;
ensure
definition: Result = (Current.order_equal (other) or
Current < other);
infix ">" (other: like Current) : BOOLEAN
-- Is `Current' strictly greater than `other'?
require
other_not_void: other /= Void;
ensure
definition: Result = (other < Current);
infix ">=" (other: like Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void: other /= Void;
ensure
definition: Result = (other <= Current);
end interface -- class PART_COMPARABLE
|
