An "array" can grow and shrink dynamically. The initial bounds of an "array" are determined when it is created. As an "array" grows (shrinks) its length increases (decreases). The low bound is always less than or equal to the high bound, except if the [tex2html_wrap2971]array is empty; in this case, [tex2html_wrap2972]a.low() = a.high() + 1. It is always the case that [tex2html_wrap2973]a.size = a.high() - a.low() + 1. The array bounds are limited to what can be indexed using ints and to a size that can be represented as an int; thus the low bound of an array must be [tex2html_wrap2962] "int_min", and the high bound and size must be [tex2html_wrap2964] "int_max".

Consider an "array" "a". The legal indexes of "a" are all integers "i" such that "a.low()" [tex2html_wrap2966] "i" [tex2html_wrap2968] "a.high()". The elements in the "array" occur at element positions [tex2html_wrap2974]a.low(), a.low() + 1, ...,; if "i" is a legal index, then we refer to the element it indexes as "a[i]". E.g., if "a" has low bound -2 and contains 1, 2 and 3, then -2, -1, and 0 are legal indexes and "a[-2]", "a[-1]", and "a[0]" are legal array elements.

The array routine "array_create" allows the new array to be created using the varying arguments form (6.1). For example

a: array[int] := array_create[int](0, .. 6, 9, 17)creates a new array with low bound 0 and containing the elements 6, 9, and 17.

Methods for type "array[T]"

empty ( ) returns (bool) % effects returns true if the array is empty, else returns false. length ( ) returns (int) % effects returns the length of the array (a count of the number of elements it contains). low ( ) returns (int) % effects returns the low bound of the array. high ( ) returns (int) % effects returns the high bound of the array. fetch (i: int) returns (T) signals (bounds) % effects if i is not a legal index in self, signals bounds. Otherwise % returns the element self[i]. bottom ( ) returns (T) signals (bounds) % effects if self is empty, signals bounds. Otherwise returns the first element of self. top ( ) returns (T) signals (bounds) % effects if self is empty, signals bounds. Otherwise, returns the last element of self. store (i: int, v: T) signals (bounds) % modifies self % effects If i is not a legal index in self, signals bounds. % Otherwise, sets the element at self[i] to v. append (x: T) % modifies self % effects If adding x to the high end of self would cause the high bound % or size of self to become too large, signals failure. % otherwise, adds x to the high end of self. remove ( ) returns (T) signals (bounds) % modifies self % effects if self is empty signals bounds. % otherwise, removes and returns the highest element of self. append_low (x: T) % modifies self % effects if adding x to the low end of self would cause the low bound % or size of self to exceed the limits, signals failure. % otherwise adds x to the low end of self. remove_low ( ) returns (T) signals (bounds) % modifies self % effects if self is empty signals bounds. % otherwise, removes and returns the lowest element of self. predict (cnt: int) % effects the method has no effect on the array state. However, it predicts % that the array will grow to have size cnt, and the append calls % that cause the array to grow may operate faster as a result % of the call on predict. set_low (lb: int) % modifies self % effects if changing the low bound of self to lb would cause its size or % high bound to become too large, signals failure. % otherwise, sets the low bound of self to lb and renumbers the % array elements accordingly. trim (lb: int, count: int) signals (negative_size, bounds) % modifies self % effects if count < 0, signals negative_size. if lb < low() or lb > high() + 1, % signals bounds. Otherwise, removes all elements with indices less than lb % or greater than lb + count - 1; the new low bound is lb. For example, % a.trim(3, 2), where a is a 5 element array[int] with low bound 0 and % containing the elements 1, 2, 3, 4, 5, changes a to have low bound 3 and % contain the two elements 4, 5. a.trim(3, 12) has the same effect. indexes ( ) yields (int) % effects yields the legal indices of self from the low bound of pre(self) to % the high bound of pre(self), where pre(self) is the value of self at % the time of the call. Note that any modifications to the array done % in the loop body do not affect the integers yielded by this method. elements ( ) yields (T) % effects The effect of x.elements() is equivalent to the following body: % for i: int in x.indexes() do % yield (x[i]) except when bounds: signal failure(...) end % end % Thus if the loop body does not modify the array, the array % elements are yielded in order. Note, however, that changes % made by the loop body can affect what is yielded. equal (a: array[T]) returns (bool) % effects returns true if self and a are the same array object. similar (a: array[T]) returns (bool) where T has similar (T) returns (bool) % effects returns true if self and a have the same size and low bound and the elements at % corresponding positions are similar (using the T similar method to do the test). copy ( ) returns (array[T]) where T has copy ( ) returns (T) % effects returns a new array with the same size and low bound as self and containing % a copy of each element of self (using T copy) in the corresponding positions. unparse ( ) returns (string) where T has unparse ( ) returns (string) % effects produces a string representation of the contents of self using the % T unparse method to produce string images of the elements. % The resulting string has the form array[\tex{$L$}: \tex{$e_L$},...,\tex{$e_H$}], % where \tex{$e_i$} is obtained by calling the T unparse method for that element, % and \tex{$L$} and \tex{$H$} are the low and high bounds of the array.Routines for type "array[T]"

array_new[T] ( ) returns (array[T]) % effects creates new empty array with a low bound of 1 array_create[T] (lb: int, els: sequence[T]) returns (array[T]) % effects creates a new array with low bound lb containing the elements of the % sequence in order; signals failure if the high bound of the % resulting array would be too large. array_generate[T] (lb: int, els: iter () yields (T)) returns (array[T]) % effects returns a new array containing the elements yielded by the % iterator in order; signals failure if the high bound of the % resulting array would be too large.

theta-questions@lcs.mit.edu