Arrays: Issues and Examples

Arrays

Sizes: One-dimensional arrays indexed by some prefix of the natural numbers. An array of size n is indexed by the set {0..(n-1)} totally ordered in the usual way. ARRAY is a spec about arrays of differing sizes, not about a single array of some fixed size. Although this spec talks about arrays of all sizes, note that there is no operation to extend an array. See the Dynamic-Array spec for such an operation.
Constructors: The Array constructors are: constant-array and update
Domain, Indicies, and apply: An array of size n has a general domain (NAT) and a defined domain (valid-indicies) consisting of the Nats from zero to n - 1 (inclusive). ARRAY employs the restrict to a subsort (Defined-Dom) technique for ensuring that array access (application) is total.
Spec: The static array spec is in: array.re

In ARRAY-K, all arrays have the same size: array-k-size They have the same operations as in the general static array spec.

Extend Static Arrays In this version, dynamic arrays are a simple definitional extension of static arrays that provide an extension operation extend-array-n to grow the array. It takes an Array, a Nat (number of slots to add), and an element to initialize the extension part.
Spec: The dynamic array spec is in: dynamic-array.re