Class ARRAY
ELKS '95

indexing

    description: "Sequences of values, all of the same type or of a %
        %conforming one, accessible through integer indices in a %
        %contiguous interval"

class interface

    ARRAY [G]

creation

    make (minindex, maxindex: INTEGER)
            -- Allocate array; set index interval to
            -- minindex .. maxindex; set all values to default.
            -- (Make array empty if minindex > maxindex.)
        ensure
            no_count: (minindex > maxindex) implies (count = 0); 
            count_constraint: (minindex <= maxindex) implies 
                (count = maxindex - minindex + 1)

    make_from_array (a: ARRAY [G])
            -- Initialize from the items of a.
            -- (Useful in proper descendants of class ARRAY,
            -- to initialize an array-like object from a manifest array.)

feature -- Initialization

    make (minindex, maxindex: INTEGER)
            -- Set index interval to minindex .. maxindex;
            -- reallocate if necessary; set all values to default.
            -- (Make array empty if minindex > maxindex.)
        ensure
            no_count: (minindex > maxindex) implies (count = 0); 
            count_constraint: (minindex <= maxindex) implies 
                (count = maxindex - minindex + 1)

    make_from_array (a: ARRAY [G])
            -- Initialize from the items of a; reallocate if
            -- necessary. (Useful in proper descendants of
            -- class ARRAY, to initialize an array-like object
            -- from a manifest array.)

feature -- Access

    entry (i: INTEGER): G
            -- Entry at index i, if in index interval
            -- (Redefinable synonym for item and infix "@".)
        require
            good_key: valid_index (i)

    frozen item (i: INTEGER): G
            -- Entry at index i, if in index interval
        require
            good_key: valid_index (i)

    frozen infix "@" (i: INTEGER): G
            -- Entry at index i, if in index interval
        require
            good_key: valid_index (i)

feature -- Measurement

    count: INTEGER
            -- Number of available indices

    lower: INTEGER
            -- Minimum index

    upper: INTEGER
            -- Maximum index

feature -- Comparison

    is_equal (other: like Current): BOOLEAN
            -- Is array made of the same items as other?
            -- (Redefined from GENERAL.)

feature -- Status report

    valid_index (i: INTEGER): BOOLEAN
            -- Is i within the bounds of the array?

feature -- Element change

    enter (v: G; i: INTEGER)
            -- Replace i-th entry, if in index interval, by v.
            -- (Redefinable synonym for put.)
    	require
            good_key: valid_index (i)
    	ensure
            inserted: item (i) = v

    force (v: like item; i: INTEGER)
            -- Assign item v to i-th entry.
            -- Always applicable: resize the array if i falls out of
            -- currently defined bounds; preserve existing items.
        ensure
            inserted: item (i) = v
            higher_count: count >= old count

    frozen put (v: like item; i: INTEGER)
            -- Replace i-th entry, if in index interval, by v.
        require
            good_key: valid_index (i)
        ensure
            inserted: item (i) = v

feature -- Resizing

    resize (minindex, maxindex: INTEGER)
            -- Rearrange array so that it can accommodate
            -- indices down to minindex and up to maxindex.
            -- Do not lose any previously entered item.
        require
            good_indices: minindex <= maxindex
        ensure
            no_low_lost: lower = minindex.min (old lower);
            no_high_lost: upper = maxindex.max (old upper)

feature -- Conversion

    to_c: POINTER
            -- Address of actual sequence of values, 
            -- for passing to external (non-Eiffel) routines.

feature -- Duplication

    copy (other: like Current)
            -- Reinitialize by copying all the items of other.
            -- (This is also used by clone.)
            -- (From GENERAL.)

invariant

    consistent_size: count = upper - lower + 1; 
    non_negative_count: count >= 0

end