树非递归遍历统一的新解法及其形式证明  

United Solution and Its Formal Proof about Non-Recursive Algorithms of Tree Traversal

作　　者：化志章[1] 杨庆红[1] 揭安全[1] 

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022

出　　处：《江西师范大学学报（自然科学版）》2010年第2期123-127,共5页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家"973"前期预研项目(2003CCA02800);国家自然科学基金(60273092);江西省自然基金(2008GQS0056);江西省教育厅科技项目(GJJ09142)资助

摘　　要：提出树遍历统一的新解法,使其非递归算法像递归算法一样简单.首先以后序遍历为例,基于结点状态标记和遍历规则提取,从遍历定义导出遍历的递推公式,由此机械获得非递归算法和循环不变式,并用形式化方法证明其正确性.之后按不同遍历定义变换公式参数,获得二叉树前序、中序和K叉树前序、后序的递推公式,所得算法比传统算法更简洁直观,表明本解法的有效性和通用性.A united solution of tree traversal is presented.It makes its non-recursive algorithms are same easy as its recursive algorithms.From the definition of postorder,by marking node states and extracting rules,the recurrence formula of postorder is derived.Then,non-recursive algorithm and its loop invariant are obtained mechanically according to the formula,their correctness are proved formally.Furthermore,some recurrence formulas of other kinds of traversals,including preorder/inorder of binary tree,and preorder/postorder of K-ary tree,are obtained by changing formula＇s parameters according to their traversal definitions,and the algorithms are more simple than the traditional.Results show that our solution is valid and united.

关 键 词：树遍历 非递归算法 循环不变式 

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