Class CHARACTER

Halstenbach Eiffel 3.1

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
      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): like Current
      -- The greater of current object and `other'
      require -- from COMPARABLE
         other_exists: other /= void
      ensure -- from COMPARABLE
         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'
      require -- from COMPARABLE
         other_exists: other /= void
      ensure -- from COMPARABLE
         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
      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'?
      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'?
      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'?
      require -- from PART_COMPARABLE
         other_exists: other /= void
      ensure then -- from COMPARABLE
         definition: Result = (other <= Current)
        
feature -- Status report

   is_alpha: BOOLEAN
      -- Is `Current' alphabetic?
      -- Alphabetic is `is_upper' or `is_lower'

   is_digit: BOOLEAN
      -- Is `Current' 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 `Current' lowercase?

   is_upper: BOOLEAN
      -- Is `Current' uppercase?
        
feature -- Element change

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

   lower: CHARACTER
      -- Lowercase value of `Current'
      -- Returns `Current' if not `is_upper'

   upper: CHARACTER
      -- Uppercase value of `Current'
      -- Returns `Current' if not `is_lower'
        
feature -- Output

   out: STRING
      -- Printable representation of character
        
feature -- Basic routines

   next: CHARACTER
      -- Next character
      require -- from CHARACTER_REF
         valid_character: item /= '%/255/'
      ensure -- from CHARACTER_REF
         valid_result: Result |-| item = 1

   previous: CHARACTER
      -- Previous character
      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 `Current'
      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 `Current'
      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 `Current' and `other'
      ensure -- from CHARACTER_REF
         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