indexing
	description: "Bounded structures that can be resized"
	library: "Gobo Eiffel Structure Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

deferred class interface
	DS_RESIZABLE [G]

feature -- Measurement

	capacity: INTEGER
			-- Maximum number of items in structure

	count: INTEGER
			-- Number of items in structure
			-- (from DS_CONTAINER)
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is current structure equal to other?
			-- (from DS_CONTAINER)
		require -- from GENERAL
			other_not_void: other /= void
		ensure -- from GENERAL
			symmetric: Result implies other.is_equal (Current);
			consistent: standard_is_equal (other) implies Result
		ensure then -- from DS_CONTAINER
			same_count: Result implies count = other.count
	
feature -- Status report

	is_empty: BOOLEAN
			-- Is structure empty?
			-- (from DS_CONTAINER)

	is_full: BOOLEAN
			-- Is structure full?
	
feature -- Removal

	wipe_out
			-- Remove all items from structure.
			-- (from DS_CONTAINER)
		ensure -- from DS_CONTAINER
			wipe_out: is_empty
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize structure so that it can contain
			-- at least n items. Do not lose any item.
		require
			n_large_enough: n >= capacity
		ensure
			capacity_set: capacity = n
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	count_constraint: count <= capacity;
	full_definition: is_full = (count = capacity);
		-- from DS_CONTAINER
	positive_count: count >= 0;
	empty_definition: is_empty = (count = 0);

end -- class DS_RESIZABLE