5
$\begingroup$

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!

$\endgroup$
  • $\begingroup$ When a mathematician says he is giving a (formal) proof, he usually means that he is giving enough details and hints so that the educated reader (depending on the intended level of the reading audience) will be able to fill in the details as much as needed, without having to be especially creative. There are actually many ways of further formalizing a proof by filling in details in a "systematic" way (i.e. thru a precise mathematical formalism). Floyd-Hoare logic is only one of them. $\endgroup$ – babou Jun 11 '13 at 9:22
  • $\begingroup$ @babou As an undergraduate major in math (although I'm a freshman), I clearly know that mathematicians almost only emphasize on non-trivial facts and the big picture. However, since I'm a novice to CS, I have no picture or well-structured intuition in my mind, therefore I need some hints to formulate a Hoare logic like proof. Consequently, I'll make rudiments clearer. $\endgroup$ – Yai0Phah Jun 11 '13 at 9:36
  • $\begingroup$ @babou Another comment: in fact I got idea about the proof. However, I felt like that my knowledge of fundamental infrastructure of validity is rare, and to test my ability, I tried to turn the proof into a Hoare-logic proof (at least, to be sure that it could be translated, if too tedious). Just like something in mathematics: the formula $F_{n+2}=F_{n+1}+F_n$ with $F_1=F_2=1$ is well-defined. However, before learning something about set theory, I don't exactly know how to illustrate it rigorously (and it's not trivial in the context of set theory). Now I'm considering the similar thing in CS. $\endgroup$ – Yai0Phah Jun 11 '13 at 10:31
  • $\begingroup$ For what I understood, your question was fair. The word "formal" can be used informally. Very formal proofs are often too tedious for human beings. However the concept is important as it leads to mechanization in computerized proof assistants, or even automatic provers, an important research topic. $\endgroup$ – babou Jun 11 '13 at 11:56
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Essentially, Knuth's "formal proof" conveys the key idea that would need to be encoded in a Hoare logic proof, and as such is just an informal proof sketch. $\endgroup$ – András Salamon Jun 11 '13 at 22:29
  • $\begingroup$ @AndrásSalamon Now I doubt whether it could be. Note that Knuth's statement is across control-flow. He makes a statement inductively that the control-flow will eventually come into another arrow of the flow chart with some property, where the Hoare logic proof is approximately step-by-step. $\endgroup$ – Yai0Phah Jun 12 '13 at 10:39
  • $\begingroup$ The general real situation is that, when I'm thinking about an algorithm, I'm pretty clear about the main idea but a bit confused about some local details. I decide to make a mathematical proposition attached to these details to ensure the validity. However, I think I should enhance my knowledge about the rudiments, which helps me immediately point out that the mathematical proposition, if informal, is essentially equivalent to a Hoare logic proposition, and I could turn the proof into Hoare logic one whenever I want. $\endgroup$ – Yai0Phah Jun 12 '13 at 10:48
  • $\begingroup$ @FrankScience, agreed that Knuth's proof is "global" while Hoare logic appears to be purely local. But ultimately for correctness one needs to reason about some set of global states that captures the notion that the algorithm makes progress toward a well-defined goal. Knuth outlined one way to capture this, and Yuval describes the idea in more detail. $\endgroup$ – András Salamon Jun 12 '13 at 11:48
  • $\begingroup$ @AndrásSalamon I don't understand clearly. However, now I doubt whether Hoare logic proof is necessary. The situation is different with the case of ZFC on which most mathematicians build theory. For example, if $S_n$ is a sequence of states, Knuth's proof is approximately: $\forall N,\exists n>N\colon P(S_n)$ where $P$ is a statement. Yuval's hint is about a Hoare logic proof. I could complete it, stack containing the ancestors unvisited. I believe that the proof is somewhat trivial. However, I don't think the proof clarifies the underlying idea, and it differs from Knuth's essentially. $\endgroup$ – Yai0Phah Jun 12 '13 at 16:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.