关键词: 后序遍历二叉树, 循环不变式, PAR方法, 非线性数据结构, DijkstraGries标准程序证明法

Abstract: 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.

Key words: postorder binarytree traversal;loop invariant;PAR method;nonlinear data structure;DijkstraGries standard proving technique