= Solution
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:
``
def display: Unit = {
print("[")
var i = 0
while (i < size) {
if (i > 0) print(", ")
print(a(slot(i)))
i += 1
}
println("]")
}
``
Assume ordinary sequential execution and successful output. The <loop invariant> is $0\leq i\leq 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>.
Back to article page
