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

非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.

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

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.