Class CHARACTER
Latest draft of the ELKS 2002 proposal incorporating ELKS 95 plus all motions
accepted to date.
(Text that appears in gray has not yet been considered in detail.)
indexing
description: "Characters, with comparison operations and an ASCII code"
expanded class interface
CHARACTER
feature -- Access
code: INTEGER
-- Associated integer value
hash_code: INTEGER
-- Hash code value
-- (From HASHABLE.)
ensure
good_hash_value: Result >= 0
feature -- Comparison
infix "<" (other: like Current): BOOLEAN
-- Is 'other' greater than current character?
-- (Inherited from COMPARABLE.)
require -- from COMPARABLE
other_exists: other /= Void
ensure -- from COMPARABLE
asymmetric: Result implies not (other < Current)
ensure then
definition: result = (code < other.code)
infix "<=" (other: like Current): BOOLEAN
-- Is current character less than or equal to other?
-- (From COMPARABLE.)
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?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (other <= Current)
infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (other < Current)
max (other: like Current): like Current
-- The greater of current object and other
-- (From COMPARABLE.)
require
other_exists: 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
-- (From COMPARABLE.)
require
other_exists: 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.
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
equal_zero: (Result = 0) = is_equal (other);
smaller: (Result = -1) = Current < other;
greater_positive: (Result = 1) = Current > other
feature -- Conversion
as_lower: like Current
-- Lower case equivalent
ensure
non_void_result:
Result /= Void
converted:
("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(item)
implies Result.item = ("abcdefghijklmnopqrstuvwxyz").item(
("ABCDEFGHIJKLMNOPQRSTUVWXYZ").index_of(item, 1))
unchanged:
not ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(item)
implies Result = Current
as_upper: like Current
-- Upper case equivalent
ensure
non_void_result:
Result /= Void
converted:
("abcdefghijklmnopqrstuvwxyz").has(item)
implies Result.item = ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").item(
("abcdefghijklmnopqrstuvwxyz").index_of(item, 1))
unchanged:
not ("abcdefghijklmnopqrstuvwxyz").has(item)
implies Result = Current
feature -- Output
out: STRING
-- Printable representation of character
-- (From GENERAL.)
invariant
irreflexive_comparison: not (Current < Current)
end
Copyright © 1995 NICE.
Eiffel and NICE are trademarks of the Nonprofit International Consortium
for Eiffel.