= Solution
A fixed-size <array> cannot implement unbounded successful insertion. \b[Either specify a bounded <double-ended queue> with an extra not-full insertion <precondition>, or retain the unbounded interface and specify a possible full-capacity failure.] Silently overwriting an endpoint would change the stated behavior. Here use the bounded contract, with a fixed positive capacity `MAX` and abstract state $|s|\leq MAX$. Both additions require $|s|<MAX$; the other <postconditions> remain unchanged. The class declaration in part (c) is interpreted as implementing this explicitly revised contract, rather than as a behavioral subtype of the unrestricted contract in part (a).
The concrete state is an <array> `a` of length `MAX`, a first-position index `head`, and an occupied-entry count `size`. Its <representation invariant> is
$$
MAX>0,\qquad a.length=MAX,\qquad 0\leq head<MAX,\qquad0\leq size\leq MAX.
$$
The <abstraction function> is $s(k)=a((head+k)\bmod MAX)$ for $0\leq k<size$. Unoccupied slots are unconstrained. Storing `size` distinguishes empty and full states even though their two circular endpoint positions coincide. `MAX=1` is valid. Using a <circular buffer> avoids shifting entries and makes every endpoint operation <constant time>.
Back to article page
