Question about the formal proof of the inorder traversing

Question

In Don Knuth's famous series of books, The Art of Computer Programming, section 2.3.1, he describes an algorithm to traverse binary tree in inorder, making use of an auxiliary stack:

T1 [Initialize.] Set stack $\rm A$ empty and set the link variable $\rm P\gets T$

T2 [$\rm P=\Lambda$?] If $\rm P=\Lambda$, go to step T4.

T3 [Stack$\rm \;\Leftarrow P$] (Now $\rm P$ points to a nonempty binary tree that is to be traversed.) push the value of $\rm P$ onto stack $\rm A$, then set $\rm P\gets LLINK(P)$

T4 [$\rm P\Leftarrow Stack$] If stack $\rm A$ is empty, the algorithm terminates; otherwise pop the top of $\rm A$ to $\rm P$.

T5 [Visit $\rm P$] Visit $\rm NODE(P)$. Then set $\rm P\gets RLINK(P)$ and return to step T2.

We can plot a flow chart of the algorithm. In the succeeding paragraph, he gives a formal proof of the algorithm:

Starting at step T2 with $\rm P$ a pointer to a binary tree of $n$ nodes and with the stack $\rm A$ containing $\rm A[1]\dotsc A[m]$ for some $m\ge 0$, the procedure of steps T2-T5 will traverse the binary tree in question, in inorder, and will then arrive at step T4 with stack $\rm A$ returned to its original value $\rm A[1]\dotsc A[m]$.

However, as far as I know, such a formal proof is quite different from the general method described in section 1.2.1:

for each box in the flow chart, that if an assertion attached to any arrow leading into the box is true before the operation in that box is performed, then all of the assertions on relevant arrows leading away from the box are true after the operation.

In fact, such a method is somewhat equivalent to Hoare logic, which is used to formally check the validity of algorithms.

Can we turn the statement mentioned to prove the traversing algorithm into a schema of Hoare logic, or the assertion-attachment of a flow chart?

Thanks!

Answer 1

It is definitely possible to analyze this algorithm using Hoare triples. The first step would be to replace the VISIT procedure calls with some more reasonable accounting mechanism, say a list that lists the visited nodes in order. You then define formally what a binary tree is and what an inorder traversal is, something along the following lines:

Tree = Leaf N | Node N LTree RTree
Inorder(Leaf N) = N
Inorder(Node N LTree RTree) = Inorder(LTree) || N || Inorder(RTree)

Here N is the "name" of the node, and || is list concatenation. Armed with these notions, it is an exercise to construct the required Hoare triples. You will probably need to come up with even more notions (for example, you will need to explain what the contents of the stack are when a node P is popped).

What do we gain from this exercise? Do we understand the algorithm any better? Probably not. But we understand how to reason precisely about algorithms, something which is useful if you plan on doing software verification or programming language theory, areas forming the so called "Theory B". If you're more of a "Theory A" type (algorithms and complexity) then, like me, you will find such exercises somewhat beside the point.