Research On Dafny Program Generation And Verification Based On Model Transformation

Today's world is an era where everything is defined by software,especially in the field of safety and security,it is necessary to ensure the reliable operation of computer programs.This reliability can be achieved by passing all possible test cases to the program,but this method is difficult to guarantee the correctness of some complex programs with an unlimited input range.The purpose of formal verification is to construct a mathematical description of the correctness of the program,but the required verification work is tedious and error-prone.The use of automatic verification tools to automate the proof process is a trend in formal verification.Dafny is a programming language and static program prover with a built-in protocol structure created by Microsoft Research.Its purpose is to verify the functional correctness of the program and fully automate the program verification process.This greatly reduces the tedious program verification process and greatly improves the reliability of the software.It must be recognized that there are no specific methods and tools for the generation of Dafny programs at this stage.Dafny programs for many problems are based on the experience of developers,and the loop invariants in Dafny programs are all from the sky,based on the developers 'design of algorithms skill level.This paper combines the algorithm programming method PAR method and the program prover Dafny to propose a model-driven Dafny program generation and verification method.Through this method,some classic problems are formalized and automatically verified by the algorithm,which greatly improves the developed algorithm program Reliability.Research work includes:1.An overview of the Dafny programming language,including grammar and protocol structure;an analysis of the Dafny automatic verification mechanism and an example description,and a manual construction proof of the Dafny program for practical problems;2.Explore a model-driven Dafny program formal generation and automatic verification method.The steps are as follows: First,the protocol transformation technology is used in the early stage of program development to get the problem's Radl algorithm from the problem Radl protocol;then,the PAR method is used to develop a new strategy to obtain the cycle invariant;finally,the Radl algorithm Based on the loop invariant,the Dafny program of the problem is obtained according to the model equivalent conversion rules,and the Dafny prover automatically verifies that the program functions correctly.3.The algorithm program development and verification of some typical problems,such as cubic sum,minimum sum,search,sorting,etc.,are solved by this method,which proves that this method can effectively improve the development efficiency,correctness and reliability of Dafny program.The double nested loop Dafny program is used to generate the equivalent transformation rules of the model.Based on this,several bubble sorting algorithm programs are generated,and a new local bubble sorting algorithm is generated.