Institutional Repository
| 后序遍历二叉树非递归算法的推导及形式化证明 | |
| Alternative Title | derivation and formal proof of non-recursive postorder binary-tree traversal algorithm |
左正康 ; 游珍; 薛锦云
| |
| 2010 | |
| Source | 计算机工程与科学
 |
| ISSN | 1007-130X |
| Volume | 32Issue:3Pages:119-123 |
| English Abstract | 开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码。实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性。 |
| Keyword | 后序遍历二叉树 循环不变式 Par方法 非线性数据结构 Dijkstra-gries标准程序证明法 |
| Department | 江西师范大学省高性能计算技术重点实验室;中国科学院软件研究所;中国科学院研究生院; |
| Language | 中文 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/9854 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | 左正康,游珍,薛锦云. 后序遍历二叉树非递归算法的推导及形式化证明[J]. 计算机工程与科学,2010,32(3):119-123. |
| APA | 左正康,游珍,&薛锦云.(2010).后序遍历二叉树非递归算法的推导及形式化证明.计算机工程与科学,32(3),119-123. |
| MLA | 左正康,et al."后序遍历二叉树非递归算法的推导及形式化证明".计算机工程与科学 32.3(2010):119-123. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 后序遍历二叉树非递归算法的推导及形式化证（444KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment