work in progress | character

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.