deferred class ARRAYED_COLLECTION [E_]

Features exported to ANY

Common root for ARRAY, FAST_ARRAY and RING_ARRAY.

Direct parents

conformant parents

COLLECTION

Known children

conformant children

ARRAY, FAST_ARRAY, RING_ARRAY

Summary

exported features

Implementation of deferred:

Interfacing with C:

Accessing:

Writing:

Adding:

Modification:

Removing:

Looking and Searching:

Looking and comparison:

Printing:

Agents based features:

Other features:

Indexing:

Counting:

Other features:

Details

capacity: INTEGER

Internal storage capacity in number of item.

upper: INTEGER

Upper index bound.

deferred subarray (min: INTEGER, max: INTEGER): ARRAYED_COLLECTION [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

first: E_

The very first item.

See also last, item.

require

  • not is_empty

ensure

  • definition: Result = item(lower)

last: E_

The last 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, add_last, 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 last 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, remove_last.

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

deferred item (i: INTEGER): E_

Item at the corresponding index i.

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

require

  • valid_index(i)

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)

deferred 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

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

deferred set_all_with (v: E_)

Set all items with value v.

See also set_slice_with.

ensure

  • 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

deferred 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 add_last, first, last, add.

ensure

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

deferred add_last (element: E_)

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

See also add_first, last, first, add.

ensure

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

append_collection (other: COLLECTION[E_])

Append other to Current.

See also add_last, add_first, add.

require

  • other /= Void

ensure

  • count = other.count + old count

deferred 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

deferred copy (other: ARRAYED_COLLECTION [E_])

Reinitialize by copying all the items of other.

require

  • same_dynamic_type(other)

ensure

  • is_equal(other)

deferred 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

deferred remove_first

Remove the first element of the collection.

See also remove_last, remove, remove_head.

require

  • not is_empty

ensure

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

deferred 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

deferred 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, remove_last.

require

  • valid_index(index)

ensure

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

frozen clear
This feature is obsolete: Now use `clear_count' or `clear_count_and_capacity' (july 17th 2004).
deferred 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

  • is_empty: count = 0

deferred 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

  • is_empty: count = 0

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.

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)

deferred 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))

deferred 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)

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)

deferred 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)

deferred 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

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)

deferred is_equal (other: ARRAYED_COLLECTION [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)

deferred is_equal_map (other: ARRAYED_COLLECTION [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

deferred 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.

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

deferred occurrences (element: E_): INTEGER

Number of occurrences of element using is_equal for comparison.

See also fast_occurrences, index_of.

ensure

  • Result >= 0

deferred fast_occurrences (element: E_): INTEGER

Number of occurrences of element using basic = for comparison.

See also occurrences, index_of.

ensure

  • Result >= 0

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

deferred slice (min: INTEGER, max: INTEGER): ARRAYED_COLLECTION [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

reverse

Reverse the order of the elements.

ensure

  • count = old count

deferred lower: INTEGER

Minimum index.

See also upper, valid_index, item.

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)

deferred count: INTEGER

Number of available indices.

See also is_empty, lower, upper.

ensure

  • definition: Result = upper - lower + 1

deferred is_empty: BOOLEAN

Is collection empty ?

See also count.

ensure

  • definition: Result = (count = 0)

deferred get_new_iterator: ITERATOR[E_]

Class invariant