二叉树排序非递归算法推导及形式化证明  

The Derivation and Formal Proof of Binary Tree Sorting Non-Recursive Algorithm

作　　者：左正康[1] 方越 黄箐 廖云燕[1] 王渊[2] 王昌晶[1] ZUO Zhengkang;FANG Yue;HUANG Qing;LIAO Yunyan;WANG Yuan;WANG Changjing(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China;College of Software,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

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

出　　处：《江西师范大学学报（自然科学版）》2020年第6期625-632,共8页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(61862033,61762049,61902162);江西省自然科学基金(20202BABL202026,2020BABL202025,20202BAB202015);国家留学基金(202008360094)资助项目.

摘　　要：非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.The development of loop invariants for recursive problems of nonlinear data structures are always difficult problems in formal development.In this paper,an approach for the derivation and formal proof of binary tree non-recursive algorithm are researched,and the non-recursive Apla(Abstract Programming Language)algorithm of binary tree sorting algorithm and its exact and simple loop invariant are derived.Then,the correctness of the algorithm is proved by Dijkstra-Gries standard proving technique.In the end,the PAR platform C++program automatic generation system automatically generates C++code.The experimental results of the example simplify the derivation and proof of the algorithm program and are useful for the direction for the exploration of loop invariant of non-recursive algorithm for recursive problems,which has guiding significance for the formal proof of algorithm program for nonlinear data structure.

关 键 词：二叉树类非递归算法 循环不变式 PAR平台 Dijkstra-Gries标准程序证明法 非线性数据结构 

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