indexing
	description: "Stacks (Last-In, First-Out) implemented with arrays"
	library: "Gobo Eiffel Structure Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

class interface
	DS_ARRAYED_STACK [G]

create 

	make (n: INTEGER)
			-- (from DS_ARRAYED_LIST)
		require -- from DS_ARRAYED_LIST
			positive_n: n >= 0
		ensure -- from DS_ARRAYED_LIST
			empty: is_empty;
			capacity_set: capacity = n

	make_equal (n: INTEGER)
			-- (from DS_ARRAYED_LIST)
		require -- from DS_ARRAYED_LIST
			positive_n: n >= 0
		ensure -- from DS_ARRAYED_LIST
			empty: is_empty;
			capacity_set: capacity = n

feature -- Access

	item: G
			-- Last item in list
			-- (from DS_ARRAYED_LIST)
		require -- from DS_BILINEAR
			not_empty: not is_empty
		require -- from DS_INDEXABLE
			not_empty: not is_empty
		ensure -- from DS_BILINEAR
			has_last: has (Result)

	searcher: DS_ARRAYED_LIST_SEARCHER [G]
			-- Stack searcher
	
feature -- Measurement

	capacity: INTEGER
			-- Maximum number of items in list
			-- (from DS_ARRAYED_LIST)

	count: INTEGER
			-- Number of items in list
			-- (from DS_ARRAYED_LIST)

	occurrences (v: G): INTEGER
			-- Number of times v appears in structure
			-- (Use searcher's comparison criterion.)
			-- (from DS_SEARCHABLE)
		ensure -- from DS_SEARCHABLE
			positive: Result >= 0;
			has: has (v) implies Result >= 1
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is list equal to other?
			-- (from DS_ARRAYED_LIST)
		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

	extendible (nb: INTEGER): BOOLEAN
			-- May list be extended with nb items?
			-- (from DS_ARRAYED_LIST)
		require -- DS_ARRAYED_LIST
			precursor: True
		require -- from DS_EXTENDIBLE
			positive_n: n >= 0
		ensure then -- from DS_ARRAYED_LIST
			enough_space: Result implies capacity >= count + nb
		ensure then -- from DS_ARRAYED_LIST
			enough_space: Result implies capacity >= count + nb

	has (v: G): BOOLEAN
			-- Does structure incluse v?
			-- (Use searcher's comparison criterion.)
			-- (from DS_SEARCHABLE)
		ensure -- from DS_SEARCHABLE
			not_empty: Result implies not is_empty

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

	is_full: BOOLEAN
			-- Is structure full?
			-- (from DS_RESIZABLE)
	
feature -- Element change

	append (other: DS_LINEAR [G])
			-- Add items of other to end of list.
			-- Resize structure if needed.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_DYNAMIC
			other_not_void: other /= void
		require -- from DS_INDEXABLE
			other_not_void: other /= void
		ensure -- from DS_DYNAMIC
			new_count: count = old count + other.count
		ensure -- from DS_INDEXABLE
			new_count: count = old count + other.count

	extend (other: DS_LINEAR [G])
			-- Add items of other to end of list.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_DYNAMIC
			other_not_void: other /= void;
			extendible: extendible (other.count)
		require -- from DS_INDEXABLE
			other_not_void: other /= void;
			extendible: extendible (other.count)
		ensure -- from DS_DYNAMIC
			new_count: count = old count + other.count
		ensure -- from DS_INDEXABLE
			new_count: count = old count + other.count

	force (v: G)
			-- Add v to end of list.
			-- Resize structure if needed.
			-- (from DS_ARRAYED_LIST)
		ensure -- from DS_DYNAMIC
			one_more: count = old count + 1;
			inserted: item = v
		ensure -- from DS_INDEXABLE
			one_more: count = old count + 1;
			inserted: item = v

	put (v: G)
			-- Add v to end of list.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_DYNAMIC
			extendible: extendible (1)
		require -- from DS_INDEXABLE
			extendible: extendible (1)
		ensure -- from DS_DYNAMIC
			one_more: count = old count + 1;
			inserted: item = v
		ensure -- from DS_INDEXABLE
			one_more: count = old count + 1;
			inserted: item = v

	replace (v: G)
			-- Replace top item by v.
		require -- from DS_STACK
			not_empty: not is_empty
		ensure -- from DS_STACK
			same_count: count = old count;
			replaced: item = v
	
feature -- Resizing

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

	copy (other: like Current)
			-- Copy other to current list.
			-- (from DS_ARRAYED_LIST)
		require -- from GENERAL
			other_not_void: other /= void;
			type_identity: same_type (other)
		ensure -- from GENERAL
			is_equal: is_equal (other)
	
feature -- Setting

	set_searcher (a_searcher: like searcher)
			-- Set searcher to a_searcher.
			-- (from DS_SEARCHABLE)
		require -- from DS_SEARCHABLE
			a_searcher_not_void: a_searcher /= void
		ensure -- from DS_SEARCHABLE
			searcher_set: searcher = a_searcher
	
feature -- removal

	keep (n: INTEGER)
			-- Keep n first items in list.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_EXTENDIBLE
			valid_n: 0 <= n and n <= count
		ensure -- from DS_EXTENDIBLE
			new_count: count = n

	prune (n: INTEGER)
			-- Remove n last items from list.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_DYNAMIC
			valid_n: 0 <= n and n <= count
		require -- from DS_INDEXABLE
			valid_n: 0 <= n and n <= count
		ensure -- from DS_DYNAMIC
			new_count: count = old count - n
		ensure -- from DS_INDEXABLE
			new_count: count = old count - n

	remove
			-- Remove item at end of list.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_DYNAMIC
			not_empty: not is_empty
		require -- from DS_INDEXABLE
			not_empty: not is_empty
		ensure -- from DS_DYNAMIC
			one_less: count = old count - 1
		ensure -- from DS_INDEXABLE
			one_less: count = old count - 1

	wipe_out
			-- Remove all items from list.
			-- (from DS_ARRAYED_LIST)
		ensure -- from DS_CONTAINER
			wipe_out: is_empty
	
invariant

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

end -- class DS_ARRAYED_STACK