Derivation And Formal Proof Of Non-recursive Algorithm For Binary Tree Queue Recursion Relation Problems

The development of loop invariants for non-recursive algorithms for nonlinear data structure problems is always a difficulty in formal development.As a widely used one to many nonlinear data structures,tree not only has the pointing relation among data,but also has the hierarchy relation.Because of the complexity of tree structure,in order to simplify the operation and storage,we generally convert tree to binary tree processing.Therefore,the derivation and formal proof of binary tree non-recursive algorithm is of great value.Combined with PAR method and PAR platform,this paper derives and formalizes the non-recursive algorithm of binary tree queue recursion relation problem.The binary tree problems are partitioned to find recursion relations.A strategy of derivation and formal proof is presented for a class of problems with queue recurrence relations.It also explores the commonness and characteristics of loop invariants of non-recursive algorithms for binary tree queue recursion problem.We can divide the binary tree queue recursion problems into three kinds of derivation problems.Three kinds of recursive relation examples of binary tree queue are derived,and the recursive relation expression and loop invariant expression is obtained,from which a general non-recursive Apla(Abstract Programming Language)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.The proposed strategy greatly improves the efficiency and effectiveness of developing generic algorithm programs at the same time.A new direction is pointed out for finding the common among the loop invariants of various non-recursive algorithms for binary tree queue relationship problems.It is instructive for the derivation and formal proof of algorithm program of nonlinear data structure.