Eiffeldoc: ARRAY

+

Point of view

All features

class ARRAY [E_]

Summary

General purpose resizable ARRAYs as they are define in the Eiffel language definition. The lower bound can be any arbitrary value, even a negative one.

This implementation uses only one chunk of memory, the storage area which is a NATIVE_ARRAY. One must keep in mind that this internal storage area is always kept left align. Thus, you can expect good performances while using an ARRAY to modelize a stack behavior with add_last / last / remove_last. Conversely add_first and remove_first are likely to slow down your program if they are too often used. If the fact that lower is always stuck to 0 is not a problem for you, also consider FAST_ARRAY to get better performances.

Direct parents: Inherit list: ARRAYED_COLLECTION, COLLECTION; Insert list: NATIVE_ARRAY_COLLECTOR

Class invariant

valid_bounds: lower <= upper + 1
capacity >= upper - lower + 1
capacity > 0 implies storage.is_not_null

Overview

Creation features

default_create

Default creation method.
make (min_index: INTEGER_32, max_index: INTEGER_32)

Prepare the array to hold values for indexes in range [min_index .. max_index].
with_capacity (needed_capacity: INTEGER_32, low: INTEGER_32)

Create an empty array with capacity initialized at least to needed_capacity and lower set to low.
from_collection (model: TRAVERSABLE[E_])

Initialize the current object with the contents of model.

Features

{}

default_create

Default creation method.

lower: INTEGER_32

Lower index bound.

Creation and Modification:

make (min_index: INTEGER_32, max_index: INTEGER_32)

Prepare the array to hold values for indexes in range [min_index .. max_index].
with_capacity (needed_capacity: INTEGER_32, low: INTEGER_32)

Create an empty array with capacity initialized at least to needed_capacity and lower set to low.

{}

ensure_capacity_and_bounds (needed_capacity: INTEGER_32, low: INTEGER_32, up: INTEGER_32)

Modification:

resize (min_index: INTEGER_32, max_index: INTEGER_32)

Resize to bounds min_index and max_index.
reindex (new_lower: INTEGER_32)

Change indexing to take in account the expected new_lower index.

Implementation of deferred:

count: INTEGER_32

Number of available items in the hoard.
is_empty: BOOLEAN

Is the hoard empty ?

See also count.
subarray (min: INTEGER_32, max: INTEGER_32): ARRAY [E_]

New collection consisting of items at indexes in [min .. max].
item (i: INTEGER_32): E_

Item at the corresponding index i.
put (element: E_, i: INTEGER_32)

Make element the item at index i.
force (element: E_, index: INTEGER_32)

Make element the item at index, enlarging the collection if necessary (new bounds except index are initialized with default values).
copy (other: ARRAY [E_])

Reinitialize by copying all the items of other.
set_all_with (v: E_)

Set all items with value v.
remove_first

Remove the first element of the collection.
remove_head (n: INTEGER_32)

Remove the n elements of the collection.
remove (index: INTEGER_32)

Remove the item at position index.
clear_count

Discard all items (is_empty is True after that call).
clear_count_and_capacity

Discard all items (is_empty is True after that call).
add_first (element: E_)

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

Add a new item at the end : count is increased by one.
from_collection (model: TRAVERSABLE[E_])

Initialize the current object with the contents of model.
all_default: BOOLEAN

Do all items have their type's default value?
occurrences (element: E_): INTEGER_32

Number of occurrences of element using is_equal for comparison.
fast_occurrences (element: E_): INTEGER_32

Number of occurrences of element using basic = for comparison.
first_index_of (element: E_): INTEGER_32

Give the index of the first occurrence of element using is_equal for comparison.
index_of (element: E_, start_index: INTEGER_32): INTEGER_32

Using is_equal for comparison, gives the index of the first occurrence of element at or after start_index.
reverse_index_of (element: E_, start_index: INTEGER_32): INTEGER_32

Using is_equal for comparison, gives the index of the first occurrence of element at or before start_index.
fast_first_index_of (element: E_): INTEGER_32

Give the index of the first occurrence of element using basic = for comparison.
fast_index_of (element: E_, start_index: INTEGER_32): INTEGER_32

Using basic = for comparison, gives the index of the first occurrence of element at or after start_index.
fast_reverse_index_of (element: E_, start_index: INTEGER_32): INTEGER_32

Using basic = comparison, gives the index of the first occurrence of element at or before start_index.
fast_is_equal (other: ARRAY [E_]): BOOLEAN

Do both collections have the same lower, upper, and items?
is_equal (other: ARRAY [E_]): BOOLEAN

Do both collections have the same lower, upper, and items?
slice (min: INTEGER_32, max: INTEGER_32): ARRAY [E_]

New collection consisting of items at indexes in [min..max].
new_iterator: ITERATOR[E_]

Garbage collector tuning (very low-level):

{}

mark_native_arrays

For performance reasons, the unused area of storage is always left as it is when some elements are removed.

Implement manifest generic creation (very low-level):

{}

manifest_make (needed_capacity: INTEGER_32, initial_lower: INTEGER_32)

Manifest creation of an ARRAY[E_] with lower set to initial_lower.
manifest_put (index: INTEGER_32, element: E_)

Accessing:

infix "@" (i: INTEGER_32): E_

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

Writing:

swap (i1: INTEGER_32, i2: INTEGER_32)

Swap item at index i1 with item at index i2.
set_slice_with (v: ANY, lower_index: INTEGER_32, upper_index: INTEGER_32)

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

Set every item to its default value.

Adding:

add (element: ANY, index: INTEGER_32)

Add a new element at rank index : count is increased by one and range [index .. upper] is shifted right by one position.
append_collection (other: COLLECTION[E_])

Append other to Current.
append_traversable (other: TRAVERSABLE[E_])

Append other to Current.

Removing:

remove_last

Remove the last item.
remove_tail (n: INTEGER_32)

Remove the last n item(s).

Looking and Searching:

has (x: ANY): BOOLEAN

Look for x using is_equal for comparison.
fast_has (x: ANY): BOOLEAN

Look for x using basic = for comparison.
last_index_of (element: ANY): INTEGER_32

Using is_equal for comparison, gives the index of the last occurrence of element at or before upper.
fast_last_index_of (element: ANY): INTEGER_32

Using basic = for comparison, gives the index of the last occurrence of element at or before upper.

Looking and comparison:

is_equal_map (other: ARRAY [E_]): BOOLEAN

Do both collections have the same lower, upper, and items?
same_items (other: COLLECTION[E_]): BOOLEAN

Do both collections have the same items?

Other features:

replace_all (old_value: ANY, new_value: ANY)

Replace all occurrences of the element old_value by new_value using is_equal for comparison.
fast_replace_all (old_value: ANY, new_value: ANY)

Replace all occurrences of the element old_value by new_value using basic = for comparison.
move (lower_index: INTEGER_32, upper_index: INTEGER_32, distance: INTEGER_32)

Move range lower_index ..
reverse

Reverse the order of the elements.

Implement manifest generic creation:

{}

manifest_semicolon_check: BOOLEAN

enumerate: ENUMERATE[E_]

Other features:

get_new_iterator: ITERATOR[E_]

Agent-based features:

for_each (action: PROCEDURE[TUPLE[TUPLE 1[E_]]])

Apply action to every item of Current.
for_all (test: FUNCTION[TUPLE[TUPLE 1[E_]]]): BOOLEAN

Do all items satisfy test?
exists (test: FUNCTION[TUPLE[TUPLE 1[E_]]]): BOOLEAN

Does at least one item satisfy test?
aggregate (action: FUNCTION[TUPLE[TUPLE 2[E_, E_], E_]], initial: E_): E_

Aggregate all the elements starting from the initial value.

Printing:

out_in_tagged_out_memory

Append terse printable representation of current object in tagged_out_memory.

generation: INTEGER_32

{}

next_generation

Agent-based features:

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

Apply action to every item of Current.

{}

_inline_agent1 (a: ROUTINE[TUPLE[TUPLE 1[E_]]], e: E_)

Indexing:

upper: INTEGER_32

Maximum index.
valid_index (i: INTEGER_32): BOOLEAN

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

Accessing:

first: E_

The very first item.
last: E_

The last item.

{ARRAYED_COLLECTION, ARRAYED_COLLECTION_HANDLER}

storage: NATIVE_ARRAY[E_]

Internal access to storage location.
from_external (a_storage: POINTER, a_capacity: INTEGER_32)

capacity: INTEGER_32

Internal storage capacity in number of item.

Interfacing with C:

to_external: POINTER

Gives C access into the internal storage of the ARRAY.

{ARRAYED_COLLECTION}

set_upper (new_upper: INTEGER_32)

{}

mark_item (native_array: NATIVE_ARRAY[E_], index: INTEGER_32)

To be used _only_ inside the definition of mark_native_arrays.

default_create

effective procedure

{}

Default creation method.

It is used when no creation method is specified if allowed. Note it may be renamed.

lower: INTEGER_32

writable attribute

Lower index bound.

make (min_index: INTEGER_32, max_index: INTEGER_32)

effective procedure

Prepare the array to hold values for indexes in range [min_index .. max_index].

Set all values to default. When max_index = min_index - 1, the array is_empty.

require

valid_bounds: min_index <= max_index + 1

ensure

lower_set: lower = min_index
upper_set: upper = max_index
items_set: all_default

with_capacity (needed_capacity: INTEGER_32, low: INTEGER_32)

effective procedure

Create an empty array with capacity initialized at least to needed_capacity and lower set to low.

require

needed_capacity >= 0

ensure

is_empty
needed_capacity <= capacity
lower = low

ensure_capacity_and_bounds (needed_capacity: INTEGER_32, low: INTEGER_32, up: INTEGER_32)

effective procedure

{}

require

up >= low - 1
needed_capacity >= up - low + 1

ensure

needed_capacity <= capacity
lower = low
upper = up
all_default

resize (min_index: INTEGER_32, max_index: INTEGER_32)

effective procedure

Resize to bounds min_index and max_index.

Do not lose any item whose index is in both [lower .. upper] and [min_index .. max_index]. New positions if any are initialized with the appropriate default value.

require

min_index <= max_index + 1

ensure

lower = min_index
upper = max_index

reindex (new_lower: INTEGER_32)

effective procedure

Change indexing to take in account the expected new_lower index.

The upper index is translated accordingly.

ensure

lower = new_lower
count = old count

count: INTEGER_32

effective function

Number of available items in the hoard.

See also is_empty

ensure

Result >= 0

is_empty: BOOLEAN

effective function

Is the hoard empty ?

See also count.

ensure

definition: Result = count = 0

subarray (min: INTEGER_32, max: INTEGER_32): ARRAY [E_]

effective function

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

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

item (i: INTEGER_32): E_

effective function

Item at the corresponding index i.

See also lower, upper, valid_index.

require

valid_index(i)

valid_index(i)

valid_index(i)

valid_index(i)

put (element: E_, i: INTEGER_32)

effective procedure

Make element the item at index i.

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

require

valid_index(i)

valid_index(i)

ensure

item(i) = element
count = old count

force (element: E_, index: INTEGER_32)

effective procedure

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(

True

) or else (

index >= lower

) ensure

lower = index.min(old lower)
upper = index.max(old upper)
item(index) = element

copy (other: ARRAY [E_])

effective procedure

Reinitialize by copying all the items of other.

require

not immutable
same_dynamic_type(other)

not immutable
same_dynamic_type(other)

not immutable
same_dynamic_type(other)

not immutable
same_dynamic_type(other)

ensure

is_equal(other)

set_all_with (v: E_)

effective procedure

Set all items with value v.

See also set_slice_with.

ensure

count = old count

remove_first

effective procedure

Remove the first element of the collection.

See also remove_last, remove, remove_head.

require

not is_empty

not is_empty

ensure

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

remove_head (n: INTEGER_32)

effective procedure

Remove the n elements of the collection.

See also remove_tail, remove, remove_first.

require

n > 0 and n <= count

n > 0 and n <= count

ensure

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

remove (index: INTEGER_32)

effective procedure

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)

valid_index(index)

ensure

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

clear_count

effective procedure

Discard all items (is_empty is True after that call).

If possible, the actual implementation 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

effective procedure

Discard all items (is_empty is True after that call).

If possible, the actual implementation 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

add_first (element: E_)

effective procedure

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

add_last (element: E_)

effective procedure

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

from_collection (model: TRAVERSABLE[E_])

effective procedure

Initialize the current object with the contents of model.

require

model /= Void
useful_work: model /= Current

model /= Void
useful_work: model /= Current

ensure

lower = model.lower
upper = model.upper
count = model.count

all_default: BOOLEAN

effective function

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_32

effective function

Number of occurrences of element using is_equal for comparison.

See also fast_occurrences, index_of.

ensure

Result >= 0

fast_occurrences (element: E_): INTEGER_32

effective function

Number of occurrences of element using basic = for comparison.

See also occurrences, index_of.

ensure

Result >= 0

first_index_of (element: E_): INTEGER_32

effective function

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(element, lower)

index_of (element: E_, start_index: INTEGER_32): INTEGER_32

effective function

Using is_equal for comparison, gives the index of the first occurrence of element at or after start_index.

Return upper + 1 if the search for element failed.

See also fast_index_of, reverse_index_of, first_index_of.

ensure

Result.in_range(start_index, upper + 1)
valid_index(Result) implies (create {SAFE_EQUAL}).test(element, item(Result))

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

effective function

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)

valid_index(start_index)

ensure

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

fast_first_index_of (element: E_): INTEGER_32

effective function

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

definition: Result = fast_index_of(element, lower)

fast_index_of (element: E_, start_index: INTEGER_32): INTEGER_32

effective function

Using basic = for comparison, gives the index of the first occurrence of element at or after start_index.

Answer upper + 1 when element when the search fail.

See also index_of, fast_reverse_index_of, fast_first_index_of.

ensure

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

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

effective function

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)

valid_index(start_index)

ensure

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

fast_is_equal (other: ARRAY [E_]): BOOLEAN

effective function

Do both collections have the same lower, upper, and items?

The basic = is used for comparison of items.

See also is_equal, same_items.

ensure

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

is_equal (other: ARRAY [E_]): BOOLEAN

effective function

Do both collections have the same lower, upper, and items?

Feature is_equal is used for comparison of items.

See also fast_is_equal, same_items.

require

other /= Void

other /= Void

other /= Void

other /= Void

ensure

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

slice (min: INTEGER_32, max: INTEGER_32): ARRAY [E_]

effective function

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

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

ensure

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

new_iterator: ITERATOR[E_]

effective function

ensure

Result /= Void
Result.generation = generation

mark_native_arrays

effective procedure

{}

For performance reasons, the unused area of storage is always left as it is when some elements are removed.

No time is lost to clean the released area with a Void or a 0 value. (Look for example the remove_last implementation.) Thus, the unused area of storage may contains references of actually unreachable objects. The following mark_native_arrays actually replace the default behavior (the call is automatic) in order to mark only reachable objects.

manifest_make (needed_capacity: INTEGER_32, initial_lower: INTEGER_32)

effective procedure

{}

Manifest creation of an ARRAY[E_] with lower set to initial_lower.

require

needed_capacity > 0

manifest_put (index: INTEGER_32, element: E_)

effective procedure

{}

require

index >= 0

index >= 0

infix "@" (i: INTEGER_32): E_

frozen

effective function

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_32, i2: INTEGER_32)

effective procedure

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: ANY, lower_index: INTEGER_32, upper_index: INTEGER_32)

effective procedure

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

effective procedure

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

add (element: ANY, index: INTEGER_32)

deferred procedure

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

append_collection (other: COLLECTION[E_])

effective procedure

Append other to Current.

This feature is obsolete: Use `append_traversable' instead.

append_traversable (other: TRAVERSABLE[E_])

effective procedure

Append other to Current.

See also add_last, add_first, add.

require

other /= Void

ensure

count = other.count + old count

remove_last

deferred procedure

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

deferred procedure

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

has (x: ANY): BOOLEAN

effective function

Look for x using is_equal for comparison.

See also fast_has, index_of, fast_index_of.

ensure

definition: Result = valid_index(first_index_of(x))

fast_has (x: ANY): BOOLEAN

effective function

Look for x using basic = for comparison.

See also has, fast_index_of, index_of.

ensure

definition: Result = valid_index(fast_first_index_of(x))

last_index_of (element: ANY): INTEGER_32

effective function

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_last_index_of (element: ANY): INTEGER_32

effective function

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)

is_equal_map (other: ARRAY [E_]): BOOLEAN

effective function

Do both collections have the same lower, upper, and items?

This feature is obsolete: Use `is_equal' instead.

same_items (other: COLLECTION[E_]): BOOLEAN

effective function

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 yield True with Current indexed in range [1..2] and other indexed in range [2..3]).

See also is_equal, fast_is_equal.

require

other /= Void

ensure

Result implies count = other.count

replace_all (old_value: ANY, new_value: ANY)

deferred procedure

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}).test(old_value, new_value) implies occurrences(old_value) = 0

fast_replace_all (old_value: ANY, new_value: ANY)

deferred procedure

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

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

effective procedure

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

deferred procedure

Reverse the order of the elements.

ensure

count = old count

manifest_semicolon_check: BOOLEAN

is False

constant attribute

{}

enumerate: ENUMERATE[E_]

effective function

get_new_iterator: ITERATOR[E_]

frozen

effective function

This feature is obsolete: Use `new_iterator' instead. This historical SmartEiffel feature is badly named.

for_each (action: PROCEDURE[TUPLE[TUPLE 1[E_]]])

effective procedure

Apply action to every item of Current.

See also for_all, exists, aggregate.

require

action /= Void

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

effective function

Do all items satisfy test?

See also for_each, exists, aggregate.

require

test /= Void

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

effective function

Does at least one item satisfy test?

See also for_each, for_all, aggregate.

require

test /= Void

aggregate (action: FUNCTION[TUPLE[TUPLE 2[E_, E_], E_]], initial: E_): E_

effective function

Aggregate all the elements starting from the initial value.

See also for_each, for_all, exists.

require

action /= Void

out_in_tagged_out_memory

effective procedure

Append terse printable representation of current object in tagged_out_memory.

require

locked: tagged_out_locked

ensure

still_locked: tagged_out_locked
not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))

generation: INTEGER_32

writable attribute

next_generation

effective procedure

{}

ensure

generation > old generation

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

frozen

effective procedure

Apply action to every item of Current.

This feature is obsolete: Use `for_each` instead. This feature is not secure because it accepts a FUNCTION, the result of which is lost.

_inline_agent1 (a: ROUTINE[TUPLE[TUPLE 1[E_]]], e: E_)

frozen

effective procedure

{}

upper: INTEGER_32

deferred function

Maximum index.

See also lower, valid_index, item.

valid_index (i: INTEGER_32): BOOLEAN

effective function

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

See also lower, upper, item.

ensure

definition: Result = lower <= i and i <= upper

first: E_

deferred function

The very first item.

See also last, item.

require

not is_empty

ensure

definition: Result = item(lower)

last: E_

deferred function

The last item.

See also first, item.

require

not is_empty

ensure

definition: Result = item(upper)

storage: NATIVE_ARRAY[E_]

writable attribute

{ARRAYED_COLLECTION, ARRAYED_COLLECTION_HANDLER}

Internal access to storage location.

from_external (a_storage: POINTER, a_capacity: INTEGER_32)

effective procedure

{ARRAYED_COLLECTION, ARRAYED_COLLECTION_HANDLER}

require

a_capacity > 0 implies a_storage.is_not_null

ensure

storage.to_external = a_storage
capacity = a_capacity

capacity: INTEGER_32

writable attribute

Internal storage capacity in number of item.

to_external: POINTER

effective function

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

effective procedure

{ARRAYED_COLLECTION}

mark_item (native_array: NATIVE_ARRAY[E_], index: INTEGER_32)

{}

To be used _only_ inside the definition of mark_native_arrays.

Forces the garbage collector to continue the marking process on the index-th element of the native_array. The element at index can be Void or not Void (the Void-ness test performed inside the mark_item itself).