Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming / 3 / b / Solution

A fixed-capacity implementation needs a bounded contract: $|A|+|B|\le \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 isThe abstraction function isBoth lists are top-first. The unoccupied middle interval has length right - left; a push is possible exactly when this is positive. Thus every array position can be used by either stack, avoiding a rigid half-array allocation.