= Solution
A fixed-capacity implementation needs a bounded contract: \b[$|A|+|B|\leq\mathrm{MAX}$], and a push requires strict inequality. Pop <preconditions> and all successful-operation <postconditions> remain unchanged. An implementation that rejects full-array pushes cannot satisfy an unbounded specification promising every push; the capacity restriction must be part of the agreed <abstract data type>, or its resource-failure behavior must be specified.
Use one <array> and two boundaries `left` and `right`. The first <stack> occupies indices below `left` and grows rightwards; the second occupies indices at least `right` and grows leftwards. The <representation invariant> is
$$
\mathrm{data.length}=\mathrm{MAX},\qquad 0\leq\mathrm{left}\leq\mathrm{right}\leq\mathrm{MAX}.
$$
The <abstraction function> is
$$
A=\operatorname{reverse}(\mathrm{data}[0..\mathrm{left})),\qquad B=\mathrm{data}[\mathrm{right}..\mathrm{MAX}).
$$
Both <lists> are top-first. The unoccupied middle interval has length `right - left`; a push is possible exactly when this is positive. Thus \b[every <array> position can be used by either <stack>], avoiding a rigid half-array allocation.
\Image[/past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2021/imperative-programming-shared-array-stacks.png]
{title=Original shared-array double-stack layout: two stacks grow towards a common free interval}
Back to article page
