Past exam of the year 1 of the computer science course of the University of Oxford / 2003 / Functional programming, data structures and algorithms, procedural programming, and digital hardware / 7

The representation invariant for the array stack is $0\le s.n\le N$, with live entries at positions $0,\dots ,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

In a preorder traversal, visit the root before the left subtree, then visit the right subtree. The NIL test prevents visiting or dereferencing an empty binary tree:

PROCEDURE preorder(t : node);
BEGIN
  IF t # NIL THEN
    visit(t);
    preorder(t.left);
    preorder(t.right)
  END
END preorder;

Structural induction proves correctness. The empty binary tree has nothing to visit. For a nonempty root, visit(t) comes first; by the induction hypothesis, each recursive call visits exactly its own subtree in preorder traversal order, and the left call finishes before the right begins. Each recursive call receives a strictly smaller finite tree, proving termination. Assuming visit neither changes the child links nor fails to return, the procedure therefore realizesFor $m$ nodes, overhead is $\Theta (m+1)$ and recursion depth is $O(h+1)$ for height $h$, in addition to the cost of visit. The claim presumes an actual binary tree; cycles or shared nodes in an arbitrary pointer graph need additional handling if each object is to be visited exactly once.