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