|
|||||
|
|
| 后序遍历二叉树非递归算法的推导及形式化证明 | |
| 引用本文： | 左正康,游珍,薛锦云.后序遍历二叉树非递归算法的推导及形式化证明[J].计算机工程与科学,2010,32(3):119-123. |
| 作者姓名： | 左正康 游珍 薛锦云 |
| 作者单位： | 1. 江西师范大学省高性能计算技术重点实验室,江西,南昌,330022;中国科学院软件研究所,北京,100190中国科学院研究生院,北京,100049 2. 江西师范大学省高性能计算技术重点实验室,江西,南昌,330022 3. 江西师范大学省高性能计算技术重点实验室,江西,南昌,330022;中国科学院软件研究所,北京,100190 |
| 基金项目： | 国家自然科学基金资助项目(60573080,60773054);;江西师范大学青年成才基金资助项目(1474);;江西省自然科学基金资助项目(2008GQS0056) |
| 摘 要： | 开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码。实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性。 |
| 关 键 词： | 后序遍历二叉树 循环不变式 PAR方法 非线性数据结构 Dijkstra-Gries标准程序证明法 |
| 收稿时间： | 2008-03-24 |
| 修稿时间： | 2009-07-06 |
Derivation and Formal Proof of Non-Recursive Postorder Binary-Tree Traversal Algorithm |
|
| ZUO Zheng-kang,YOU Zhen,XUE Jin-yun.Derivation and Formal Proof of Non-Recursive Postorder Binary-Tree Traversal Algorithm[J].Computer Engineering & Science,2010,32(3):119-123. | |
| Authors: | ZUO Zheng-kang YOU Zhen XUE Jin-yun |
| Affiliation: | 1.Key Laboratory for High-Performance Computing Technology/a>;Jiangxi Normal University/a>;Nanchang 330022/a>;2.Institute of Software/a>;Chinese Academy of Sciences/a>;Beijing 100190/a>;3.Graduate University of the Chinese Academy of Sciences/a>;Beijing 100049/a>;China |
| 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 algori... |
| Keywords: | postorder binary-tree traversal loop invariant PAR method non-linear data structure Dijkstra-Gries standard proving technique |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 | |
| 点击此处可从《计算机工程与科学》下载全文 | |