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

该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类问题是基于2个母算法的功能加以实现的,由此派生出3类问题.首先,对这3类派生问题进行推导,得到递...

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

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.