后序遍历二叉树非递归算法的推导及形式化证明  

Derivation and Formal Proof of Non-Recursive Postorder Binary-Tree Traversal Algorithm

作　　者：左正康[1,2,3] 游珍[1] 薛锦云[1,2] 

机构地区：[1]江西师范大学省高性能计算技术重点实验室,江西南昌330022 [2]中国科学院软件研究所,北京100190 [3]中国科学院研究生院,北京100049

出　　处：《计算机工程与科学》2010年第3期119-123,共5页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(60573080;60773054);江西师范大学青年成才基金资助项目(1474);江西省自然科学基金资助项目(2008GQS0056)

摘　　要：开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码。实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性。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.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]