Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 4 / d

Place this object method inside the concrete class. Its precondition is the representation invariant; its postcondition is that the abstract data type state is unchanged and its left-to-right contents have been printed in bracket notation followed by a newline:Assume ordinary sequential execution and successful output. The loop invariant is $0\le i\le size$, unchanged representation, and output consisting of [ followed by precisely the first $i$ abstract values, separated by commas and spaces. The loop variant $size-i$ decreases. At exit the closing bracket completes the required display, including [] for emptiness. This takes $O(size+1)$ output operations and constant space.

The successive abstract sequences are $[10]$, $[20,10]$, $[20,10,30]$, $[10,30]$, $[10,30,40]$, $[10,30,40,10]$, $[10,30,40]$, $[10,30,40,15]$, and finally $[30,40,15]$. The three removals return $20$, $10$, and $10$, respectively. With the display convention in part (i), the output isThe capacity-four bound is never exceeded. The abstract trace is independent of which physical array slots wrap around.