Development Of Several Binary Tree Algorithms And Isabelle Machine-Aided Proof

With the development of computers,software has played an increasingly important role in all walks of life.Since the launch of the "Reliable Software Basic Research" major research plan in 2007,China has invested a large amount of scientific research funds.Among them,the development tools and supporting platforms for trusted software,and the construction and verification of trusted software are the main goals of the research plan.Algorithms are the soul of computer software,and the study of algorithms with nonlinear complex structures(such as trees and graphs)has always been a hotspot at home and abroad.The tree structure is a typical non-linear data structure.It can support powerful search algorithms,effectively allocate memory space and provide regular data storage.The development and verification of the tree structure algorithm is a challenging problem in the field of formal software and trusted software research.Binary trees are the most representative.Most of the algorithms that use binary tree structure processing are not only simple to write,but also more efficient.The application field of binary tree algorithm is very wide,such as data decompression,information encryption,memory management,network communication and cluster computing,etc.The binary tree algorithm can be recursive and non-recursive,where the recursive algorithm has high recursive cost(additional stack space allocation and multiple function calls)and dangerous(stack overflow),in system programming for mission-critical tasks(such as aviation and NASA probe vehicles),recursive calls are completely prohibited.The non-recursive algorithm is more efficient,so it is particularly important to develop a highly reliable binary tree non-recursive algorithm.This paper combines the PAR method and the interactive theorem proving tool Isabelle to develop and machine-assisted prove three typical binary tree algorithms.This method not only overcomes the tediousness and error-proneness of traditional manual verification,but also greatly improves the reliability and credibility of the developed algorithm program.The successful development and verification of several examples illustrate the effectiveness and feasibility of the method.The main work of this article includes:1.Propose a method that combines the PAR method and the interactive theorem prover Isabelle to develop the binary tree algorithm and machine-aided proof.The algorithm developed by the PAR method is non-recursive,which improves the efficiency of the algorithm;the developed algorithm is machine-aided to prove that it not only overcomes the tediousness and error-proneness of traditional manual verification,but also greatly improve the reliability and credibility of the developed algorithm program.2.By inductively analyzing the structure and output attribute characteristics of the loop invariant of the binary tree algorithm,the binary tree algorithm is divided into three categories.By discovering the commonality between each type of algorithm,it is very helpful to simplify the development and verification process.3.Successfully developed and verified a series of binary tree non-recursive algorithms,including: binary tree pre-order,in-order,post-order,level traversal,calculate the internal path length of the binary tree,exchange the left and right children of all nodes of the binary tree,binary tree sorting add,delete,modify,and check operations,judge whether the binary tree is a full binary tree,and judge whether the binary tree is a balanced binary tree.This is the first formal verification of a series of non-recursive and efficient binary tree algorithms.4.On this basis,Isabelle is used to define the data types,related operations and auxiliary functions of the commonly used binary tree data structure to form a binary tree algorithm theorem proof library,which is conducive to future reuse and constructs more complex verification.