class interface KL_STRING_ROUTINES

feature(s) from KL_STRING_ROUTINES
   --  Initialization

   make (n: INTEGER): STRING
      --  Create an empty string. Try to allocate space
      --  for at least n characters.

      require
         non_negative_n: n >= 0
      ensure
         string_not_void: Result /= Void;
         empty_string: Result.count = 0

   make_buffer (n: INTEGER): STRING
      --  Create a new string containing n characters.

      require
         non_negative_n: n >= 0
      ensure
         string_not_void: Result /= Void;
         count_set: Result.count = n

feature(s) from KL_STRING_ROUTINES
   --  Status report

   is_integer (a_string: STRING): BOOLEAN
      --  Is a_string only made up of digits?

      require
         a_string_not_void: a_string /= Void

feature(s) from KL_STRING_ROUTINES
   --  Access

   case_insensitive_hash_code (a_string: STRING): INTEGER
      --  Hash code value of a_string which doesn't
      --  take case sensitivity into account

      require
         a_string_not_void: a_string /= Void
      ensure
         hash_code_positive: Result >= 0

feature(s) from KL_STRING_ROUTINES
   --  Comparison

   same_case_insensitive (s1, s2: STRING): BOOLEAN
      --  Are s1 and s2 made up of the same
      --  characters (case insensitive)?

      require
         s1_not_void: s1 /= Void;
         s2_not_void: s2 /= Void

feature(s) from KL_STRING_ROUTINES
   --  Conversion

   to_lower (a_string: STRING): STRING
      --  Lower case version of a_string
      --  (Do not alter a_string.)

      require
         a_string_not_void: a_string /= Void
      ensure
         lower_string_not_void: Result /= Void;
         same_count: Result.count = a_string.count -- 			definition: forall i in 1..a_string.count,
 -- 				Result.item (i) = a_string.item (i).to_lower

   to_upper (a_string: STRING): STRING
      --  Upper case version of a_string
      --  (Do not alter a_string.)

      require
         a_string_not_void: a_string /= Void
      ensure
         lower_string_not_void: Result /= Void;
         same_count: Result.count = a_string.count -- 			definition: forall i in 1..a_string.count,
 -- 				Result.item (i) = a_string.item (i).to_upper

feature(s) from KL_STRING_ROUTINES
   --  Resizing

   resize_buffer (a_string: STRING; n: INTEGER)
      --  Resize a_string so that it contains n characters.
      --  Do not lose any previously entered characters.

      require
         a_string_not_void: a_string /= Void;
         n_large_enough: n >= a_string.count
      ensure
         count_set: a_string.count = n


end of KL_STRING_ROUTINES