= Solution
The representation invariant for the <array> <stack> is $0\leq s.n\leq N$, with live entries at positions $0,\ldots,s.n-1$ and the top at `s.n-1` when nonempty. The following <Oberon> procedures use the given <data types>:
``
PROCEDURE makeEmpty(VAR s : stack);
BEGIN
s.n := 0
END makeEmpty;
PROCEDURE isEmpty(s : stack) : BOOLEAN;
BEGIN
RETURN s.n = 0
END isEmpty;
PROCEDURE push(VAR s : stack; t : node);
BEGIN
s.a[s.n] := t;
s.n := s.n+1
END push;
PROCEDURE pop(VAR s : stack) : node;
VAR t : node;
BEGIN
s.n := s.n-1;
t := s.a[s.n];
s.a[s.n] := NIL;
RETURN t
END pop;
``
For `push`, the supplied <precondition> `s.n < N` makes the old `s.n` a valid free index. For `pop`, the <precondition> `s.n > 0` makes the decremented index the old top. Setting the vacated entry to `NIL` avoids retaining a reference to the removed <binary tree>; it does not deallocate that <binary tree>. `makeEmpty` need not clear inactive entries for the abstract <stack> behavior. None of these procedures has a loop. Each changes or inspects a constant number of fields, so its logical work is <constant time>; an implementation of the specified by-value `isEmpty` parameter may additionally copy the fixed-capacity record. The essential update rule is
$$
\boxed{\text{push writes then increments; pop decrements then reads}.}
$$
Back to article page
