class STACK [E_]

All features

A Stack of elements of type E_.

Direct parents

non-conformant parents

FAST_ARRAY

Summary

creation features

exported features

Creation and modification:

Modification:

Implementation of deferred:

Implement manifest generic creation.

Implementation of deferred:

Interfacing with C:

Accessing:

Writing:

Adding:

Removing:

Looking and Searching:

Looking and comparison:

Printing:

Agents based features:

Other features:

Implement manifest generic creation.

Indexing:

Details

make

ensure

  • is_empty

make (new_count: INTEGER)

Make array with range [0 .. new_count - 1]. When new_count = 0 the array is empty.

require

  • new_count >= 0

ensure

  • count = new_count
  • capacity >= old capacity
  • all_default

with_capacity (needed_capacity: INTEGER)

Create an empty array with at least needed_capacity.

require

  • needed_capacity >= 0

ensure

  • capacity >= needed_capacity
  • is_empty

from_collection (model: COLLECTION[E_])

Initialize the current object with the contents of model.

require

  • model /= Void
  • useful_work: model /= Current

ensure

  • count = model.count

make

ensure

  • is_empty

get_new_iterator: ITERATOR[E_]
lower: INTEGER

Frozen lower bound.

make (new_count: INTEGER)

Make array with range [0 .. new_count - 1]. When new_count = 0 the array is empty.

require

  • new_count >= 0

ensure

  • count = new_count
  • capacity >= old capacity
  • all_default

with_capacity (needed_capacity: INTEGER)

Create an empty array with at least needed_capacity.

require

  • needed_capacity >= 0

ensure

  • capacity >= needed_capacity
  • is_empty

resize (new_count: INTEGER)

Resize the array. When new_count is greater than count, new positions are initialized with appropriate default values.

require

  • new_count >= 0

ensure

  • count = new_count
  • capacity >= old capacity

is_empty: BOOLEAN

Is collection empty ?

See also count.

ensure

  • definition: Result = (count = 0)

item (i: INTEGER): E_

Item at the corresponding index i.

See also lower, upper, valid_index, put, swap.

require

  • valid_index(i)

put (element: E_, i: INTEGER)

Make element the item at index i.

See also lower, upper, valid_index, item, swap, force.

require

  • valid_index(i)

ensure

  • item(i) = element
  • count = old count

add_first (element: E_)

Add a new item in first position : count is increased by one and all other items are shifted right.

See also push, first, top, add.

ensure

  • first = element
  • count = 1 + old count
  • lower = old lower
  • upper = 1 + old upper

add_last (element: E_)

Add a new item at the end : count is increased by one.

See also add_first, top, first, add.

ensure

  • last = element
  • count = 1 + old count
  • lower = old lower
  • upper = 1 + old upper

count: INTEGER

Number of available indices.

See also is_empty, lower, upper.

ensure

  • definition: Result = upper - lower + 1

clear_count

Discard all items (is_empty is True after that call). If possible, the actual implementation is supposed to keep its internal storage area in order to refill Current in an efficient way.

See also clear_count_and_capacity.

ensure

  • capacity = old capacity
  • is_empty: count = 0

clear_count_and_capacity

Discard all items (is_empty is True after that call). If possible, the actual implementation is supposed to release its internal storage area for this memory to be used by other objects.

See also clear_count.

ensure

  • capacity = old capacity
  • is_empty: count = 0

copy (other: STACK [E_])

Copy other onto Current.

require

  • same_dynamic_type(other)

ensure

  • is_equal(other)

set_all_with (v: E_)

Set all items with value v.

See also set_slice_with.

ensure

  • count = old count

from_collection (model: COLLECTION[E_])

Initialize the current object with the contents of model.

require

  • model /= Void
  • useful_work: model /= Current

ensure

  • count = model.count

is_equal (other: STACK [E_]): BOOLEAN

Do both collections have the same lower, upper, and items? The basic = is used for comparison of items.

See also is_equal_map, same_items.

require

  • other /= Void

ensure

  • Result implies lower = other.lower and upper = other.upper
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

is_equal_map (other: STACK [E_]): BOOLEAN

Do both collections have the same lower, upper, and items? Feature is_equal is used for comparison of items.

See also is_equal, same_items.

ensure

  • Result implies lower = other.lower and upper = other.upper

all_default: BOOLEAN

Do all items have their type's default value? Note: for non Void items, the test is performed with the is_default predicate.

See also clear_all.

occurrences (element: E_): INTEGER

Number of occurrences of element using is_equal for comparison.

See also fast_occurrences, index_of.

ensure

  • Result >= 0

fast_occurrences (element: E_): INTEGER

Number of occurrences of element using basic = for comparison.

See also occurrences, index_of.

ensure

  • Result >= 0

index_of (element: E_): INTEGER

Warning, this feature will change in the near future. Warning: this feature will have soon one extra argument as the one in class STRING.

It is better to use first_index_of right now (Oct 6th 2005).

ensure

  • Result.in_range(lower, upper + 1)
  • valid_index(Result) implies (create {SAFE_EQUAL[E_]}.default_create).test(element, item(Result))

reverse_index_of (element: E_, start_index: INTEGER): INTEGER

Using is_equal for comparison, gives the index of the first occurrence of element at or before start_index. Search is done in reverse direction, which means from the start_index down to the lower index . Answer lower -1 when the search fail.

See also fast_reverse_index_of, last_index_of, index_of.

require

  • valid_index(start_index)

ensure

  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result).is_equal(element)

first_index_of (element: E_): INTEGER

Give the index of the first occurrence of element using is_equal for comparison. Answer upper + 1 when element is not inside.

See also fast_first_index_of, index_of, last_index_of, reverse_index_of.

ensure

  • definition:

    Result = index_of(c, lower)

fast_index_of (element: E_): INTEGER

Warning, this feature will change in the near future. Warning: this feature will have soon one extra argument as the one in class STRING.

It is better to use fast_first_index_of right now (Oct 6th 2005).

ensure

  • Result.in_range(lower, upper + 1)
  • valid_index(Result) implies element = item(Result)

fast_reverse_index_of (element: E_, start_index: INTEGER): INTEGER

Using basic = comparison, gives the index of the first occurrence of element at or before start_index. Search is done in reverse direction, which means from the start_index down to the lower index . Answer lower -1 when the search fail.

See also reverse_index_of, fast_index_of, fast_last_index_of.

require

  • valid_index(start_index)

ensure

  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result) = element

subarray (min: INTEGER, max: INTEGER): STACK [E_]

New collection consisting of items at indexes in [min .. max]. Result has the same dynamic type as Current. See also slice.

require

  • lower <= min
  • max <= upper
  • min <= max + 1

ensure

  • same_dynamic_type(Result)
  • Result.count = max - min + 1
  • Result.lower = min or Result.lower = 0

slice (min: INTEGER, max: INTEGER): STACK [E_]

New collection consisting of items at indexes in [min..max]. Result has the same dynamic type as Current. The lower index of the Result is the same as lower.

See also from_collection, move, replace_all.

require

  • lower <= min
  • max <= upper
  • min <= max + 1

ensure

  • same_dynamic_type(Result)
  • Result.count = max - min + 1
  • Result.lower = lower

force (element: E_, index: INTEGER)

Make element the item at index, enlarging the collection if necessary (new bounds except index are initialized with default values).

See also put, item, swap.

require

  • index >= lower

ensure

  • upper = index.max(old upper)
  • item(index) = element

remove_first

Remove the first element of the collection.

See also pop, remove, remove_head.

require

  • not is_empty

ensure

  • lower = old lower
  • count = old count - 1
  • lower = old lower + 1 xor upper = old upper - 1

remove_head (n: INTEGER)

Remove the n elements of the collection.

See also remove_tail, remove, remove_first.

require

  • n > 0 and n <= count

ensure

  • count = old count - n
  • lower = old lower + n xor upper = old upper - n

remove (index: INTEGER)

Remove the item at position index. Followings items are shifted left by one position.

See also remove_first, remove_head, remove_tail, pop.

require

  • valid_index(index)

ensure

  • count = old count - 1
  • upper = old upper - 1

get_new_iterator: ITERATOR[E_]
manifest_make (needed_capacity: INTEGER)

Manifest creation of a FAST_ARRAY[E_].

require

  • needed_capacity > 0

manifest_put (index: INTEGER, element: E_)

require

  • index >= 0

storage: NATIVE_ARRAY[E_]

Internal access to storage location.

capacity: INTEGER

Internal storage capacity in number of item.

upper: INTEGER

Upper index bound.

first: E_

The very first item.

See also top, item.

require

  • not is_empty

ensure

  • definition: Result = item(lower)

last: E_

The top item.

See also first, item.

require

  • not is_empty

ensure

  • definition: Result = item(upper)

add (element: E_, index: INTEGER)

Add a new element at rank index : count is increased by one and range [index .. upper] is shifted right by one position.

See also add_first, push, append_collection.

require

  • index.in_range(lower, upper + 1)

ensure

  • item(index) = element
  • count = 1 + old count
  • upper = 1 + old upper

remove_last

Remove the top item.

See also remove_first, remove, remove_tail.

require

  • not is_empty

ensure

  • count = old count - 1
  • upper = old upper - 1

remove_tail (n: INTEGER)

Remove the last n item(s).

See also remove_head, remove, pop.

require

  • n > 0 and n <= count

ensure

  • count = old count - n
  • upper = old upper - n

replace_all (old_value: E_, new_value: E_)

Replace all occurrences of the element old_value by new_value using is_equal for comparison.

See also fast_replace_all, move.

ensure

  • count = old count
  • not (create {SAFE_EQUAL[E_]}.default_create).test(old_value, new_value) implies occurrences(old_value) = 0

fast_replace_all (old_value: E_, new_value: E_)

Replace all occurrences of the element old_value by new_value using basic = for comparison.

See also replace_all, move.

ensure

  • count = old count
  • old_value /= new_value implies fast_occurrences(old_value) = 0

to_external: POINTER

Gives C access into the internal storage of the ARRAY. Result is pointing the element at index lower.

NOTE: do not free/realloc the Result. Resizing of the array

      can makes this pointer invalid.

require

  • not is_empty

ensure

  • Result.is_not_null

set_upper (new_upper: INTEGER)
frozen @ (i: INTEGER): E_

The infix notation which is actually just a synonym for item.

See also item.

require

  • valid_index(i)

ensure

  • definition: Result = item(i)

swap (i1: INTEGER, i2: INTEGER)

Swap item at index i1 with item at index i2.

See also item, put.

require

  • valid_index(i1)
  • valid_index(i2)

ensure

  • item(i1) = old item(i2)
  • item(i2) = old item(i1)
  • count = old count

set_slice_with (v: E_, lower_index: INTEGER, upper_index: INTEGER)

Set all items in range [lower_index .. upper_index] with v.

See also set_all_with.

require

  • lower_index <= upper_index
  • valid_index(lower_index)
  • valid_index(upper_index)

ensure

  • count = old count

clear_all

Set every item to its default value. The count is not affected.

See also clear, all_default.

ensure

  • stable_upper: upper = old upper
  • stable_lower: lower = old lower
  • all_default

append_collection (other: COLLECTION[E_])

Append other to Current.

See also push, add_first, add.

require

  • other /= Void

ensure

  • count = other.count + old count

frozen clear
This feature is obsolete: Now use `clear_count' or `clear_count_and_capacity' (july 17th 2004).
has (x: E_): BOOLEAN

Look for x using is_equal for comparison.

See also fast_has, index_of, fast_index_of.

fast_has (x: E_): BOOLEAN

Look for x using basic = for comparison.

See also has, fast_index_of, index_of.

last_index_of (element: E_): INTEGER

Using is_equal for comparison, gives the index of the last occurrence of element at or before upper. Search is done in reverse direction, which means from the upper down to the lower index . Answer lower -1 when the search fail.

See also fast_last_index_of, reverse_index_of, index_of.

ensure

  • definition: Result = reverse_index_of(element, upper)

fast_first_index_of (element: E_): INTEGER

Give the index of the first occurrence of element using basic = for comparison. Answer upper + 1 when element is not inside.

See also first_index_of, last_index_of, fast_last_index_of.

ensure

  • Result.in_range(lower, upper + 1)
  • valid_index(Result) implies element = item(Result)

fast_last_index_of (element: E_): INTEGER

Using basic = for comparison, gives the index of the last occurrence of element at or before upper. Search is done in reverse direction, which means from the upper down to the lower index . Answer lower -1 when the search fail.

See also fast_reverse_index_of, last_index_of.

ensure

  • definition: Result = fast_reverse_index_of(element, upper)

same_items (other: COLLECTION[E_]): BOOLEAN

Do both collections have the same items? The basic = is used for comparison of items and indices are not considered (for example this routine may yeld True with Current indexed in range [1..2] and other indexed in range [2..3]).

See also is_equal_map, is_equal.

require

  • other /= Void

ensure

  • Result implies count = other.count

frozen fill_tagged_out_memory

Append a viewable information in tagged_out_memory in order to affect the behavior of out, tagged_out, etc.

do_all (action: ROUTINE[TUPLE[TUPLE 1[E_]]])

Apply action to every item of Current.

See also for_all, exists.

for_all (test: PREDICATE[TUPLE[TUPLE 1[E_]]]): BOOLEAN

Do all items satisfy test?

See also do_all, exists.

exists (test: PREDICATE[TUPLE[TUPLE 1[E_]]]): BOOLEAN

Does at least one item satisfy test?

See also do_all, for_all.

move (lower_index: INTEGER, upper_index: INTEGER, distance: INTEGER)

Move range lower_index .. upper_index by distance positions. Negative distance moves towards lower indices. Free places get default values.

See also slice, replace_all.

require

  • lower_index <= upper_index
  • valid_index(lower_index)
  • valid_index(lower_index + distance)
  • valid_index(upper_index)
  • valid_index(upper_index + distance)

ensure

  • count = old count

reverse

Reverse the order of the elements.

ensure

  • count = old count

manifest_semicolon_check: BOOLEAN
valid_index (i: INTEGER): BOOLEAN

True when i is valid (i.e., inside actual bounds).

See also lower, upper, item.

ensure

  • definition: Result = (lower <= i and i <= upper)

Class invariant