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

作     者：左正康 游珍 薛锦云 ZUO Zheng-kang;YOU Zhen;XUE Jin-yun

作者机构：江西师范大学省高性能计算技术重点实验室江西南昌330022 中国科学院软件研究所北京100190 中国科学院研究生院北京100049 

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

出 版 物：《计算机工程与科学》 (Computer Engineering & Science)

年 卷 期：2010年第32卷第3期

页      码：119-123页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1007-130X.2010.03.031

馆 藏 号：203121005...