= Solution
Store the bottom of the <stack> at index zero and the top at the last occupied index:
``
class Stack {
private val MAX = 1000
private val data = new Array[Tree](MAX)
private var used = 0
// Pre: used < MAX.
def push(t: Tree): Unit = {
require(used < MAX, "Stack full")
data(used) = t
used += 1
}
// Pre: used > 0.
def pop: Tree = {
require(used > 0, "Stack empty")
used -= 1
val result = data(used)
data(used) = null
result
}
// Pre: true.
def isEmpty: Boolean = used == 0
}
``
The <representation invariant> is that `data.length==MAX`, $0\leq used\leq MAX$, and unused slots from `used` onwards contain null references. Occupied slots contain the stored `Tree` references; the <stack> itself need not forbid null values. The <abstraction function>, written with the first <sequence> element at the top, is
$$
\alpha(data,used)=[data(used-1),data(used-2),\ldots,data(0)].
$$
Initially this is the empty <sequence>. `push` prepends its argument, `pop` removes and returns the first abstract element, and `isEmpty` reports whether the abstract <sequence> is empty. These <postconditions> follow directly from the index changes. Clearing a popped slot avoids retaining an otherwise unused <tree> reference. All three operations take \b[$O(1)$ time]. No loops are needed.
Back to article page
