home *** CD-ROM | disk | FTP | other *** search
- -- Part of SmallEiffel -- Read DISCLAIMER file -- Copyright (C)
- -- Dominique COLNET and Suzanne COLLIN -- colnet@loria.fr
- --
- deferred class COMPARABLE
- --
- -- All class handling COMPARABLE object with a total order relation
- -- should inherit from this class.
- --
-
- inherit ANY redefine is_equal end;
-
- feature {ANY}
-
- infix "<" (other: like Current): BOOLEAN is
- -- Is 'Current' strictly less than 'other'?
- require
- other_exists: other /= Void
- deferred
- ensure
- asymmetric: Result implies not (other < Current);
- end;
-
- infix "<=" (other: like Current): BOOLEAN is
- -- Is 'Current' less or equal 'other'?
- require
- other_exists: other /= Void
- do
- Result := not (Current > other)
- ensure
- definition: Result = (Current < other) or is_equal(other);
- end;
-
- infix ">" (other: like Current): BOOLEAN is
- -- Is 'Current' strictly greater than 'other'?
- require
- other_exists: other /= Void
- do
- Result := (other < Current)
- ensure
- definition: Result = (other < Current)
- end;
-
- infix ">=" (other: like Current): BOOLEAN is
- -- Is 'Current' greater or equal than 'other'?
- require
- other_exists: other /= Void
- do
- Result := not (Current < other)
- ensure
- definition: Result = (other <= Current)
- end;
-
- is_equal(other: like Current): BOOLEAN is
- do
- if Current < other then
- elseif other < Current then
- else
- Result := true;
- end;
- ensure then
- trichotomy: Result = (not (Current < other)
- and not (other < Current));
- end;
-
- compare(other: like Current): INTEGER is
- -- Compare 'Current' with 'other'.
- -- '<' <==> Result < 0
- -- '>' <==> Result > 0
- -- Otherwise Result = 0.
- require
- other /= Void
- do
- if Current < other then
- Result := -1
- elseif other < Current then
- Result := 1
- end
- ensure
- (Result < 0) = (Current < other);
- (Result = 0) = not (Current < other or Current > other);
- (Result > 0) = (Current > other)
- end;
-
- min(other: like Current): like Current is
- -- Minimum of 'Current' and 'other'.
- require
- other /= Void
- do
- if Current < other then
- Result := Current
- else
- Result := other
- end;
- ensure
- Result <= Current and then Result <= other;
- compare(Result) = 0 or else other.compare(Result) = 0
- end;
-
- max(other: like Current): like Current is
- -- Maximum of 'Current' and 'other'.
- require
- other /= Void
- do
- if other < Current then
- Result := Current;
- else
- Result := other;
- end;
- ensure
- Result >= Current and then Result >= other;
- compare(Result) = 0 or else other.compare(Result) = 0
- end;
-
- end -- COMPARABLE
-