Derivation and Formal Proof of Non-Recursive Postorder Binary-Tree Traversal Algorithm
Xue Jin-yun · Computer Engineering and Science · 2010
Developing loop invariants of algorithms containing non-linear data structure is generally regarded as a difficult problem.In this paper,new strategies for developing loop invariant are introduced,and an exact and simple loop invariant of the non-recursive postorder binary-tree traversal algorithm is worked out by adopting the recursive definition technique of loop invariants and ideas of partition-and-recur.The approach considerably simplifies the process of derivation and proof of the non-recursive algorithm and avoids the blindness of developing the loop invariant.Using datatype abstraction of Apla language,which is a part of PAR,the result algorithmic program is pretty concise and easy to be proved.Finally,the core algorithm (just 4 lines in Apla) is successfully proved by Dijkstra-Gries standard proving technique,and the abstract program is transformed into C++ program by PAR platform.It is demonstrated that the recursive definition technique of loop invariant is feasible and effective for deriving and proving non-linear data structure algorithms.