Research On Loop Invariant Development Technology

Nowadays, high-reliability software is a hot issue in software development. The best way to insure the logical structure of algorithm is formal derivation and proof, and loop invariant is the key to derive and prove algorithm formally. But the development of loop invariant is always the most difficult, the most creative and the most challenging issue.Since the emergence of formal methods, many experts apply themselves to the research of loop invariant; put forward a number of technologies developing loop invariant, such as predicate abstraction, dynamic detection technology. These technologies can detect some simple loop invariants, but can not deal with complex issues.In essence, loop invariant depicts the transformation law of loop variables and the characteristics of loop. It is difficulty to get a loop invariant, especially for complex algorithm which must be fully understood.And the current loop invariant definition does not reflect the nature of loop invariant, so technologies of developing loop invariant based on the current definition are lack of right guidance, which leading blindness in the process of developing loop invariant, and also because their technical constraints, so they can not develop loop invariants of complex problems .Xue Jinyun professor and his academic team analyze a large number of algorithms, and finding the lack of current loop invariants definition, and proposing a new loop invariants definition and new loop invariants development technologies. Based on these jobs, a practical formal method -----PAR method and its development environment are formed, which play an important role in formal development method. The major work of this paper is study of the current loop invariant definition and development technology, comparing with PAR method, and pointing out the luck of current technology, as well as implementing automatic system of developing loop invariant based on the theory of PAR method. Specific research results are as follows:1. Further in-depth study of the definition of loop invariants;2. Comparing and analyzing the standard development strategy and several current development technologies, pointing out the reasons for its difficult to apply;3. Analyzing the new loop invariants definition and new loop invariants development technologies in PAR method, and proposing a way to implement the method;4. Using the Dijkstra weakest pre-condition method to validate the loop invariant developed by this system.