indexing
description: "References to objects containing a character value"
class interface
CHARACTER_REF
feature -- Access
code: INTEGER
-- Associated integer value
hash_code: INTEGER
-- Hash code value
ensure -- from HASHABLE
good_hash_value: Result >= 0
item: CHARACTER
-- Character value
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object of the same type
-- as current object and identical to it?
require -- COMPARABLE
precursor: True
require -- from GENERAL
other_not_void: other /= void
ensure then -- from COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result
max (other: CHARACTER_REF): CHARACTER
-- The greater of current object and other
require
other_exists: other /= void
min (other: CHARACTER_REF): CHARACTER
-- The smaller of current object and other
require
other_exists: other /= void
three_way_comparison (other: CHARACTER_REF): INTEGER
-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
equal_zero: (Result = 0) = is_equal (other);
smaller_negative: (Result = - 1) = (Current < other);
greater_positive: (Result = 1) = (Current > other)
infix "<" (other: like Current): BOOLEAN
-- Is other greater than current character?
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = ((Current < other) or is_equal (other))
infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other <= Current)
feature -- Status report
is_alpha: BOOLEAN
-- Is item alphabetic?
-- Alphabetic is is_upper or is_lower
is_digit: BOOLEAN
-- Is item a digit?
-- A digit is one of 0123456789
is_hashable: BOOLEAN
-- May current object be hashed?
-- (True if it is not its type's default.)
ensure -- from HASHABLE
ok_if_not_default: Result implies (Current /= default)
is_lower: BOOLEAN
-- Is item lowercase?
is_upper: BOOLEAN
-- Is item uppercase?
feature -- Element change
set_item (c: CHARACTER)
-- Make c the item value.
feature -- Conversion
lower: CHARACTER
-- Lowercase value of item
-- Returns item if not is_upper
upper: CHARACTER
-- Uppercase value of item
-- Returns item if not is_lower
feature -- Output
out: STRING
-- Printable representation of character
feature -- Basic routines
next: CHARACTER
-- Next character
require
valid_character: item /= 'ÿ'
ensure
valid_result: Result |-| item = 1
previous: CHARACTER
-- Previous character
require
valid_character: item /= '%U'
ensure
valid_result: Result |-| item = - 1
infix "+" (incr: INTEGER): CHARACTER
-- Add incr to the code of item
require
valid_upper_increment: item.code + incr <= 255;
valid_lower_increment: item.code + incr >= 0
ensure
valid_result: Result |-| item = incr
infix "-" (decr: INTEGER): CHARACTER
-- Subtract decr to the code of item
require
valid_upper_decrement: item.code - decr <= 255;
valid_lower_decrement: item.code - decr >= 0
ensure
valid_result: item |-| Result = decr
infix "|-|" (other: CHARACTER): INTEGER
-- Difference between the codes of item and other
ensure
valid_result: other + Result = item
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from COMPARABLE
irreflexive_comparison: not (Current < Current);
end -- class CHARACTER_REF