Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

kernel.elks

Class KS_COMPARABLE


Known direct descendants

KS_STRING

Features

Invariants

indexing

description

Portable interface for class COMPARABLE

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2004/12/22 22:48:16 $

revision

$Revision: 1.6 $

deferred class

KS_COMPARABLE

feature -- Comparison

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

-- Is current object less than other?
-- (ELKS 95 COMPARABLE)

require
other_not_void: other /= Void
ensure
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN

-- Is current object less than or equal to other?
-- (ELKS 95 COMPARABLE)

require
other_not_void: other /= Void
ensure
definition: Result = (Current < other or is_equal (other))
infix ">" (other: like Current): BOOLEAN

-- Is current object greater than other?
-- (ELKS 95 COMPARABLE)

require
other_not_void: other /= Void
ensure
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN

-- Is current object greater than or equal to other?
-- (ELKS 95 COMPARABLE)

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?
-- (ELKS 95 COMPARABLE)

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then
trichotomy: Result = (not (Current < other) and not (other < Current))
max (other: like Current): like Current

-- The greater of current object and other
-- (ELKS 95 COMPARABLE)

require
other_not_void: other /= Void
ensure
current_if_not_smaller: (Current >= other) implies (Result = Current)
other_if_smaller: (Current < other) implies (Result = other)
min (other: like Current): like Current

-- The smaller of current object and other
-- (ELKS 95 COMPARABLE)

require
other_not_void: other /= Void
ensure
current_if_not_greater: (Current <= other) implies (Result = Current)
other_if_greater: (Current > other) implies (Result = other)
three_way_comparison (other: like Current): INTEGER

-- If current object equal to other, 0; if smaller,
-- -1; if greater, 1.
-- (ELKS 95 COMPARABLE)

require
other_not_void: other /= Void
ensure
equal_zero: (Result = 0) = is_equal (other)
smaller_negative: (Result = -1) = (Current < other)
greater_positive: (Result = 1) = (Current > other)

invariant


-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end