Section Header

    + name := ARRAYED_COLLECTION[E];

    - comment := "Common root for ARRAY[E] and FAST_ARRAY[E].";

Section Inherit

    - parent_arrayed:ARRAYED :=

    - parent_collection:COLLECTION[E] :=

Section ARRAYED_COLLECTION, BMP_FILE, TYPES

    + storage:NATIVE_ARRAY[E];
        Internal access to storage location.

Section Public

    - element_sizeof:INTEGER <-
        The size in number of bytes for type `E'.

    + capacity:INTEGER;
        Internal storage capacity in number of item.

    + upper:INTEGER;
        Upper index bound.

    - subarray min:INTEGER to max:INTEGER :SELF <-
        New collection consisting of items at indexes in [`min' .. `max'].
        Result has the same dynamic type as `Current'.
        See also `slice'.

Implementation of deferred:


    - first:E <-

    - second:E <-

    - last :E <-

    - add element:E to index:INTEGER <-

    - remove_last <-

    - remove_tail n:INTEGER <-

    - replace_all old_value:E with new_value:E <-

    - fast_replace_all old_value:E with new_value:E <-

    - reverse <-

Interfacing with C:


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

Section ARRAYED_COLLECTION

    - set_upper new_upper:INTEGER <-

invariant

[
-? {capacity >= (upper - lower + 1)};
-? {(capacity > 0) ->> {storage.is_not_null}};
];

Section Public

    - add_last_buffer buf:FAST_ARRAY[UINTEGER_8] from beg:INTEGER to end:INTEGER <-