二叉树队列关系问题非递归算法的推导及形式化证明  

The Derivation and Formal Proof of Non-Recursive Algorithm for Binary Tree Queue Relation Problems

作　　者：左正康[1] 方越 黄志鹏 黄箐 王昌晶[1] ZUO Zhengkang;FANG Yue;HUANG Zhipeng;HUANG Qing;WANG Changjing(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

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

出　　处：《江西师范大学学报（自然科学版）》2022年第1期49-58,共10页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(61862033,61902162);江西省教育厅科技重点课题(GJJ210307);江西省自然科学基金(20202BAB202015)资助项目.

摘　　要：该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类问题是基于2个母算法的功能加以实现的,由此派生出3类问题.首先,对这3类派生问题进行推导,得到递推关系表达式和循环不变式,由此导出非递归Apla算法;然后,使用Dijkstra-Gries标准程序证明方法证明这些算法的正确性;最后,通过Apla到C++程序自动生成系统自动生成C++代码,实现了从抽象规约到具体的可执行程序的完整求精过程.The binary tree problems are partitioned to find recursion relations in this paper.A strategy of derivation and formal proof is presented for a class of problems with queue recurrence relation.Combined with the difference of postassertion of each algorithm,three strategies for developing cycle invariant are proposed,and a general cycle invariant template for this kind of problem is constructed.At the same time,it is found that this kind of problem is implemented based on the functions of the two parent algorithms,from which three kinds of problems are derived.Firstly,the representation of the three types of derived problems is deduced,and the recursive relation expressions and loop invariant are obtained,thus the non-recursive Apla algorithm is derived.Then,the correctness of the algorithm is proved by Dijkstra-Gries standard proving technique.In the end,Apla to C++program automatic generation system automatically generates C++code.The complete refinement process from abstract specification to concrete executable program is realized.

关 键 词：二叉树队列递推关系 循环不变式 Dijkstra-Gries标准程序证明法 Apla到C++程序自动生成系统 非线性数据结构 

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