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\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\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?