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

• 作者: 左正康 游珍 薛锦云
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 后序遍历二叉树 循环不变式 PAR方法 非线性数据结构 Dijkstra-Gries标准程序证明法
• 年，卷（期）: 2010,（3）
• 所属期刊栏目: 软件工程
• 页码范围: 119-123
• 页数: 5页
• 分类号: TP311
• 字数: 4929字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2010.03.031

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	薛锦云	江西师范大学省高性能计算技术重点实验室	77	745	15.0	23.0
3	游珍	江西师范大学省高性能计算技术重点实验室	5	45	5.0	5.0