Automatic Verification Of DFS Algorithm Based On Isabelle

Formal methods are based on strict mathematical and mechanized methods to reduce,construct,and verify computing systems.They are important methods to improve and ensure the quality of computing systems.Their models,technologies,and tools have become an important carrier of computing thinking.In the formal method,the formal derivation is to obtain the algorithm program through precise transformation of the problem program specification.Formal verification is based on the specification of the software to verify whether the software has the desired properties.The formal method of software makes the description of the software system more accurate,so as to reduce the problems caused by possible errors and improve the reliability of the software.Graph structure is widely used in real life.The data structure of graph is widely used in many areas of life such as highway transportation network,subway line network,network node optimization,etc.In addition,the state execution in computer systems is also based on graph data structure.Therefore,the depth-first traversal algorithm of graphs is frequently used in modern software.The reliability of these software depends to a large extent on whether the depth-first algorithm of graphs is correct and complete.The reliability verification of the depth-first algorithm uses traditional manual derivation to verify that it can no longer meet our needs.The combination of the mathematical theorem proving tool Isabelle and formal software methods can not only adapt to increasingly tedious software verification,but also avoid manual derivation and verification.Bring mistakes.Isabelle is a universal interactive theorem prover that supports higher-order logic.It allows mathematical formulas to be expressed in formal language and provides tools for proving these formulas in logical calculus.The main application is the formalization of mathematical proofs,especially formal verification,which includes proving the correctness of computer hardware or software and proving the characteristics of computer languages and protocols.The content of this article is mainly to deeply understand the verification principle and logical structure of the Isabelle system,and to explore the application of formal methods and Isabelle theorem prover in practical production.After comparing the advantages and disadvantages of several verification methods in formal methods,Choose to use Dijkstra's weakest predicate method as the verification method.In order to verify the depth-first traversal algorithm,the definition of the graph,depth-first traversal algorithm and related lemmas are added to the rule base of the Isabelle system.And combined with Dijkstra's weakest predicate method to complete the automatic verification of the depth-first traversal algorithm of the graph.These efforts ensure the reliability of the depth-first traversal algorithm and simplify the tediousness of manual derivation verification.The extended Isabelle type library enriches the definition of graph structure for future researchers.Combining formal methods with proof tools will to some extent promote the application of formal methods to actual production.