Class CHARACTER

ISE Eiffel 4.5.020

indexing

   description: "Characters, with comparison operations and an ASCII code"
   status: "See notice at end of class"
   date: "$Date: 2002/01/31 11:04:57 $"
   revision: "$Revision: 1.1 $"

expanded class interface

   CHARACTER

feature -- Access

   code: INTEGER
      -- Associated integer value
      -- (from CHARACTER_REF)

   hash_code: INTEGER
      -- Hash code value
      -- (from CHARACTER_REF)
      ensure -- from HASHABLE
         good_hash_value: Result >= 0

   item: CHARACTER
      -- Character value
      -- (from CHARACTER_REF)
        
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?
      -- (from CHARACTER_REF)
      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: like Current): CHARACTER
      -- The greater of current object and other
      -- (from CHARACTER_REF)
      require -- from CHARACTER_REF
         other_exists: other /= void

   min (other: like Current): CHARACTER
      -- The smaller of current object and other
      -- (from CHARACTER_REF)
      require -- from CHARACTER_REF
         other_exists: other /= void

   three_way_comparison (other: CHARACTER_REF): INTEGER
      -- If current object equal to other, 0;
      -- if smaller, -1; if greater, 1
      -- (from CHARACTER_REF)
      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?
      -- (from CHARACTER_REF)
      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
      -- (from CHARACTER_REF)

   is_digit: BOOLEAN
      -- Is item a digit?
      -- A digit is one of 0123456789
      -- (from CHARACTER_REF)

   is_hashable: BOOLEAN
      -- May current object be hashed?
      -- (True if it is not its type's default.)
      -- (from CHARACTER_REF)
      ensure -- from HASHABLE
         ok_if_not_default: Result implies (Current /= default)

   is_lower: BOOLEAN
      -- Is item lowercase?
      -- (from CHARACTER_REF)

   is_upper: BOOLEAN
      -- Is item uppercase?
      -- (from CHARACTER_REF)
        
feature -- Element change

   set_item (c: CHARACTER)
      -- Make c the item value.
      -- (from CHARACTER_REF)
        
feature -- Conversion

   lower: CHARACTER
      -- Lowercase value of item
      -- Returns item if not is_upper
      -- (from CHARACTER_REF)

   upper: CHARACTER
      -- Uppercase value of item
      -- Returns item if not is_lower
      -- (from CHARACTER_REF)
        
feature -- Basic routines

   next: CHARACTER
      -- Next character
      -- (from CHARACTER_REF)
      require -- from CHARACTER_REF
         valid_character: item /= 'ÿ'
      ensure -- from CHARACTER_REF
         valid_result: Result |-| item = 1

   previous: CHARACTER
      -- Previous character
      -- (from CHARACTER_REF)
      require -- from CHARACTER_REF
         valid_character: item /= '%U'
      ensure -- from CHARACTER_REF
         valid_result: Result |-| item = - 1

   infix "+" (incr: INTEGER): CHARACTER
      -- Add incr to the code of item
      -- (from CHARACTER_REF)
      require -- from CHARACTER_REF
         valid_upper_increment: item.code + incr <= 255;
         valid_lower_increment: item.code + incr >= 0
      ensure -- from CHARACTER_REF
         valid_result: Result |-| item = incr

   infix "-" (decr: INTEGER): CHARACTER
      -- Subtract decr to the code of item
      -- (from CHARACTER_REF)
      require -- from CHARACTER_REF
         valid_upper_decrement: item.code - decr <= 255;
         valid_lower_decrement: item.code - decr >= 0
      ensure -- from CHARACTER_REF
         valid_result: item |-| Result = decr

   infix "|-|" (other: CHARACTER): INTEGER
      -- Difference between the codes of item and other
      -- (from CHARACTER_REF)
      ensure -- from CHARACTER_REF
         valid_result: other + Result = item
        
feature -- Output

   out: STRING
      -- Printable representation of character
      -- (from CHARACTER_REF)
        
invariant

   -- from GENERAL
   reflexive_equality: standard_is_equal (Current);
   reflexive_conformance: conforms_to (Current);
   -- from COMPARABLE
   irreflexive_comparison: not (Current < Current);

end -- class CHARACTER