The Automatic Detection Of Loop Invariant

The reliability of the software has always been a hot issue in software development,and the use of formal methods to develop software is an effective way to protect the reliability of software,in which the key to the development of software is the analysis of the circulatory statements in the algorithm verification.And a good understanding of the cycle of the program,the focus is to be able to correctly write the cycle of the cycle of the invariant.It is one of the most challenging,the most creative and the most difficult problems in the field of algorithm programming,whether it is manual development or automatic construction.This paper is one of the research directions of the "New Concept Circulation Invariant and Its Automatic Detection Technology" project of the National Natural Science Foundation.In this paper,we first analyze the present situation of the existing definition and its development techniques at home and abroad.Then we introduce the new definition and new development strategy of the loop invariant method in the PAR method,and the guiding ideology of constructing the circular invariant in this paper.Then,the concept of the loop invariant of single-variable assignment type is introduced.Based on the existing loop invariant generation system of the team,the construction process of the algorithm of the single-variable assignment is analyzed.The program of single-variable assignment type,in the division process of its sub-problem after the sub-problem with the original structure of the problem is not the same.For the algorithm program of single-variable assignment type,we propose a way to describe the invariance in the process of dividing the single-variable assignment by using the full quantifier,and then construct the loop invariant.Finally,we use the Java language to realize the loop invariant automatic detection of single-variable assignment type,and use Isabelle theorem to prove the automatic structure of the circular invariant,compared with the traditional manual verification,with higher reliability.There are three innovation points of the research as follows:1.For a class of the algorithm program of single-variable assignment type,in the division process of its sub-problem after the sub-problem with the original structure of the problem is not the same situation,put forward a way to use the full name of the quantifier to describe its division process of the invariance,and then construct its loop invariant.2.Use the Java language to achieve the automatic detection system of the loop invariant,and increase automatically detection of the while loop program.3.Using the Isabelle which is the theorem proving device,to prove the formal correctness of the loop invariant of single-variable assignment type.