indexing
	description: "Routines that ought to be in class STRING"
	library: "Gobo Eiffel Kernel Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

class interface
	KL_STRING_ROUTINES

feature -- 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 -- 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 -- 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
	
feature -- 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

	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
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);

end -- class KL_STRING_ROUTINES