Formal Derivation Of Algorithm And Isabelle-based Automatic Verification

The continuous development of trustworthy software promotes the in-depth study of formal methods.Formal methods are equipped with strict mathematical language and exact logical semantics to ensure the correctness of the software development process.Formal methods include two parts: formal derivation and formal verification.Formal derivation is to obtain the algorithm program by the exact transformation of the program specification.Formal verification is to verify whether the software has the desired properties on the basis of the software.Formal method is very important to ensure the correctness and reliability of software.In this paper,we study the effective ways to improve the correctness of the algorithm from two aspects: formal derivation and automatic verification.In the aspect of formal derivation,using formal methods to develop program algorithm based on recursive algorithm,and through the transformation techniques of program specification of formal program specification of equivalent transformation,so as to obtain the recurrence relations and loop invariant.Finally,the algorithm program is based on the above procedure.This method not only clearly shows the design idea and process of the algorithm,but also ensures the correctness of the algorithm.In the aspect of automatic verification,the Isabelle theorem prover is chosen as the tool.Isabelle traditional application areas are mathematical theorem proving.This paper is based on the needs of verification to extend the built-in type library and rule bank,and explores the effective method of its application in the automatic verification algorithm and problem solving sequence of recursive relation automation verification.This paper analyzes the Isabelle theorem prover from three aspects and displays the theoretical proof processes of Isabelle from three parts.According to the requirements of the two aspects of this paper,we extend the type library and rule bank of Isabelle,and complete the internal form conversion,embedment and verification of the new type and rules;then base on the extended Isabelle type library and rule bank,use the backwards proof,and combine with Dijkstra's weakest predicate method to provide the basic process of automatic verification of algorithm program,and verifie some algorithm programs of problems.At the same time,in order to avoid the artificial error caused by the manual deduce recursive relation,so we combine with the above extended Isabelle rule bank to realize the further automated verification of the recursive relation deduced from the example of this paper.The results show that the proposed algorithm can improve the effectively of correctness of the algorithm program and the efficiency of correctness of the recursive relation.