Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

structure.dispenser

Class DS_ARRAYED_STACK


Direct ancestors

DS_STACK, DS_RESIZABLE, KL_IMPORTED_ANY_ROUTINES

Creation

Features

Invariants

indexing

description

Stacks (Last-In, First-Out) implemented with arrays

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 1999, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 17:50:22 $

revision

$Revision: 1.14 $

class

DS_ARRAYED_STACK [G]

inherit

DS_STACK
DS_RESIZABLE

create

make (n: INTEGER)

-- Create an empty stack and allocate
-- memory space for at least n items.
-- Use = as comparison criterion.

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

-- Create an empty stack and allocate
-- memory space for at least n items.
-- Use equal as comparison criterion.

require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
make_default

-- Create an empty stack and allocate memory
-- space for at least default_capacity items.
-- Use = as comparison criterion.

-- (From DS_CONTAINER)

ensure
empty: is_empty

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
equality_tester: KL_EQUALITY_TESTER [G]

-- Equality tester;
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

i_th (i: INTEGER): G

-- Item at index i

require
i_large_enough: i >= 1
i_small_enough: i <= count
item: G

-- Item at top of stack

-- (From DS_DISPENSER)

require
not_empty: not is_empty

feature -- Measurement

capacity: INTEGER

-- Maximum number of items in stack

-- (From DS_RESIZABLE)

count: INTEGER

-- Number of items in stack

-- (From DS_CONTAINER)

default_capacity: INTEGER

-- Initial capacity in make_default
-- (Default value: 10)

-- (From DS_RESIZABLE)

ensure
default_capacity_positive: Result >= 0
occurrences (v: G): INTEGER

-- Number of times v appears in stack
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
positive: Result >= 0
has: has (v) implies Result >= 1

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is current stack equal to other?

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

equality_tester_settable (a_tester: like equality_tester): BOOLEAN

-- Can set_equality_tester be called with a_tester
-- as argument in current state of container?
-- (Default answer: True.)

-- (From DS_SEARCHABLE)

extendible (n: INTEGER): BOOLEAN

-- May stack be extended with n items?

-- (From DS_EXTENDIBLE)

require
positive_n: n >= 0
ensure then
enough_space: Result implies capacity >= count + n
has (v: G): BOOLEAN

-- Does stack include v?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
not_empty: Result implies not is_empty
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_full: BOOLEAN

-- Is container full?

-- (From DS_RESIZABLE)

same_equality_tester (other: DS_SEARCHABLE [G]): BOOLEAN

-- Does container use the same comparison
-- criterion as other?

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: G): BOOLEAN

-- Are v and u considered equal?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

feature -- Element change

append (other: DS_LINEAR [G])

-- Add items of other to stack.
-- Add other.first first, etc.
-- Resize stack if needed.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
ensure then
new_count: count = old count + other.count
extend (other: DS_LINEAR [G])

-- Add items of other to stack.
-- Add other.first first, etc.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure then
new_count: count = old count + other.count
force (v: G)

-- Push v on stack.
-- Resize stack if needed.

-- (From DS_EXTENDIBLE)

ensure
added: has (v)
ensure then
one_more: count = old count + 1
ensure then
pushed: item = v
put (v: G)

-- Push v on stack.

-- (From DS_EXTENDIBLE)

require
extendible: extendible (1)
ensure
added: has (v)
ensure then
one_more: count = old count + 1
ensure then
pushed: item = v
replace (v: G)

-- Replace top item by v.

-- (From DS_STACK)

require
not_empty: not is_empty
ensure
same_count: count = old count
replaced: item = v

feature -- Removal

keep (n: INTEGER)

-- Keep n items in stack.

-- (From DS_DISPENSER)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
prune (n: INTEGER)

-- Remove n items from stack.

-- (From DS_DISPENSER)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
remove

-- Remove top item from stack.

-- (From DS_DISPENSER)

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
wipe_out

-- Remove all items from stack.

-- (From DS_CONTAINER)

ensure
wiped_out: is_empty

feature -- Resizing

resize (n: INTEGER)

-- Resize stack so that it can contain
-- at least n items. Do not lose any item.

-- (From DS_RESIZABLE)

require
n_large_enough: n >= capacity
ensure
capacity_set: capacity = n

feature -- Duplication

cloned_object: like Current

-- Clone of current object

-- (From KL_CLONABLE)

ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)
copy (other: like Current)

-- Copy other to current stack.

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)

feature -- Setting

set_equality_tester (a_tester: like equality_tester)

-- Set equality_tester to a_tester.
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

require
equality_tester_settable: equality_tester_settable (a_tester)
ensure
equality_tester_set: equality_tester = a_tester

feature {DS_ARRAYED_STACK} -- Implementation

storage: SPECIAL [G]

-- Storage for items of the stack

invariant

storage_not_void: storage /= Void
capacity_definition: capacity = storage.count - 1
special_routines_not_void: special_routines /= Void

-- From DS_CONTAINER
positive_count: count >= 0
empty_definition: is_empty = (count = 0)

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

-- From DS_RESIZABLE
count_constraint: count <= capacity
full_definition: is_full = (count = capacity)

end