The Research And Application Of New Strategies For Developing Loop Invariants On Recursive Problem

Formal method is efficient way which can improve reliability and productivity of software and implement software automation. The loop invariants take a very important role in the formal method. They are a key for understanding, proving and deriving an algorithmic program. At present, the loop invariants' concept and technique is widely used in many teaching materials and literatures.However existing techniques for developing loop invariants are not very perfect which bring about lacking convincing derivation and proof in large of complex algorithmic program. This leads to that many computer scientists doubt the possibility and practicability of deriving or proving algorithmic programs by loop invariant which the famous computer scientists, Dijkstra, Hoare and Gries, advocated enthusiastic.To conquer limitations of existing techniques for developing loop invariants, professor Xue Jinyun, who is imbursed under two National Nature Science Foundation of China, systematically research the theory and method of loop invariants and advanced the new definition and developing strategies for loop invariants. Based on above, he presented efficiency method of developing algorithmic program, Partition-and-Recur Approach, and its developing environment which bring into important play in formal method. This paper is inherit of Partition-and-Recur Approach and its developing environment research and is important study content of the National Nature Science Foundation project which Xue Jinyun is taking charge of.Two new strategies for developing loop invariants on recursive problem and their application in formal derivation and proof of complex algorithmic program are presented in this paper by the idea of recursive definition which Professor Xue proposed. The main achievements include:1. This paper further research the status and function of loop invariants in formal method.2. An analysis and comparison is Given about the existing techniques for developing loop invariants and the reasons are presented why they are difficult to popularize.3. Based on recursive definition idea in existing technique of developing loop invariants, two new strategies for developing loop invariants on complicated recursive problems are presented.4. Using abstract programming language, such as Apia, the specification and derivation of the algorithmic program in six typical trees, graph problem is described. The standard proof and formal derivation is implemented by two above new strategies for developing loop invariants. The algorithm in Apia is transformed into corresponding program in Delphi and C++ by the automated algorithmic transformation system that Partition-and-Recur method provided and correct result is received. These improve reliability and developing efficiency of the kind of complex algorithm.In summary, achievements in this paper can be applied to the proof and derivation of a kind of complex algorithmic program, which are easier to use and apply. There is beneficial contribution to formal ization and automation of algorithmic program.