1 
indexing 
2 

3 
description: 
4 
"Objects that may be compared according to a total order relation" 
5 

6 
note: 
7 
"The basic operation is `<' (less than); others are defined % 
8 
%in terms of this operation and `is_equal'." 
9 

10 
status: "See notice at end of class" 
11 
names: comparable, comparison; 
12 
date: "$Date$" 
13 
revision: "$Revision$" 
14 

15 
deferred class COMPARABLE inherit 
16 

17 
PART_COMPARABLE 
18 
redefine 
19 
infix "<", infix "<=", 
20 
infix ">", infix ">=", 
21 
is_equal 
22 
end 
23 

24 
feature  Comparison 
25 

26 
infix "<" (other: like Current): BOOLEAN is 
27 
 Is current object less than `other'? 
28 
deferred 
29 
ensure then 
30 
asymmetric: Result implies not (other < Current) 
31 
end 
32 

33 
infix "<=" (other: like Current): BOOLEAN is 
34 
 Is current object less than or equal to `other'? 
35 
do 
36 
Result := not (other < Current) 
37 
ensure then 
38 
definition: Result = ((Current < other) or is_equal (other)) 
39 
end 
40 

41 
infix ">" (other: like Current): BOOLEAN is 
42 
 Is current object greater than `other'? 
43 
do 
44 
Result := other < Current 
45 
ensure then 
46 
definition: Result = (other < Current) 
47 
end 
48 

49 
infix ">=" (other: like Current): BOOLEAN is 
50 
 Is current object greater than or equal to `other'? 
51 
do 
52 
Result := not (Current < other) 
53 
ensure then 
54 
definition: Result = (other <= Current) 
55 
end 
56 

57 
is_equal (other: like Current): BOOLEAN is 
58 
 Is `other' attached to an object of the same type 
59 
 as current object and identical to it? 
60 
do 
61 
Result := (not (Current < other) and not (other < Current)) 
62 
ensure then 
63 
trichotomy: Result = (not (Current < other) and not (other < Current)) 
64 
end 
65 

66 
three_way_comparison (other: like Current): INTEGER is 
67 
 If current object equal to `other', 0; 
68 
 if smaller, 1; if greater, 1 
69 
require 
70 
other_exists: other /= Void 
71 
do 
72 
if Current < other then 
73 
Result := 1 
74 
elseif other < Current then 
75 
Result := 1 
76 
end 
77 
ensure 
78 
equal_zero: (Result = 0) = is_equal (other) 
79 
smaller_negative: (Result = 1) = (Current < other) 
80 
greater_positive: (Result = 1) = (Current > other) 
81 
end 
82 

83 
max (other: like Current): like Current is 
84 
 The greater of current object and `other' 
85 
require 
86 
other_exists: other /= Void 
87 
do 
88 
if Current >= other then 
89 
Result := Current 
90 
else 
91 
Result := other 
92 
end 
93 
ensure 
94 
current_if_not_smaller: Current >= other implies Result = Current 
95 
other_if_smaller: Current < other implies Result = other 
96 
end 
97 

98 
min (other: like Current): like Current is 
99 
 The smaller of current object and `other' 
100 
require 
101 
other_exists: other /= Void 
102 
do 
103 
if Current <= other then 
104 
Result := Current 
105 
else 
106 
Result := other 
107 
end 
108 
ensure 
109 
current_if_not_greater: Current <= other implies Result = Current 
110 
other_if_greater: Current > other implies Result = other 
111 
end 
112 

113 
invariant 
114 

115 
irreflexive_comparison: not (Current < Current) 
116 

117 
indexing 
118 

119 
library: "[ 
120 
EiffelBase: Library of reusable components for Eiffel. 
121 
]" 
122 

123 
status: "[ 
124 
Copyright 19862001 Interactive Software Engineering (ISE). 
125 
For ISE customers the original versions are an ISE product 
126 
covered by the ISE Eiffel license and support agreements. 
127 
]" 
128 

129 
license: "[ 
130 
EiffelBase may now be used by anyone as FREE SOFTWARE to 
131 
develop any product, publicdomain or commercial, without 
132 
payment to ISE, under the terms of the ISE Free Eiffel Library 
133 
License (IFELL) at http://eiffel.com/products/base/license.html. 
134 
]" 
135 

136 
source: "[ 
137 
Interactive Software Engineering Inc. 
138 
ISE Building 
139 
360 Storke Road, Goleta, CA 93117 USA 
140 
Telephone 8056851006, Fax 8056856869 
141 
Electronic mail <info@eiffel.com> 
142 
Customer support http://support.eiffel.com 
143 
]" 
144 

145 
info: "[ 
146 
For latest info see awardwinning pages: http://eiffel.com 
147 
]" 
148 

149 
end  class COMPARABLE 
150 

151 

152 
