Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming resit / 5 / a / ii / Solution

Let the abstract state be the set $B$ of occupied coordinate pairs. For the Boolean array, the abstraction function is $\alpha (occupied)=\{(x,y):occupied(y)(x)\}$. Its representation invariant requires an $N\times N$ Boolean array and the downward-closure propertyThus $B$ is an order ideal for the coordinatewise partial order. Removing an upper-right rectangle preserves this property. The empty set is allowed after the losing move.

For the row-boundary array, the abstraction function and representation invariant areThe array has length $N$. Removing at $(x,y)$ replaces each row(j) for $j\ge y$ by $\min (row(j),x)$. Earlier rows are unchanged. This both implements the abstract removal and preserves the nonincreasing boundary.

Without a cached count, the Boolean representation takes $\Theta (N^2)$ for Count, $O(1)$ for Legal, $O(N^2)$ worst-case for Move, and $\Theta (N^2)$ for a full-grid Display. The boundary representation takes $\Theta (N)$ for Count, $O(1)$ for Legal, $O(N)$ worst-case for Move, and $\Theta (N^2)$ for the same full-grid Display. Their space complexities are respectively $\Theta (N^2)$ and $\Theta (N)$. A scalar cached total makes Count $O(1)$ in either representation if each move updates it consistently. The implementation below uses that cache with the boundary array, so it achieves constant-time Count and Legal, linear worst-case Move, and linear storage. Full-grid output still takes quadratic time because it emits quadratic many cell positions.