关键词: 循环不变式, PAR方法, 高可靠性软件, 谓词抽象

Abstract:

Nowadays,highreliability software is a hot issue in software development. The best way to insure the logical structure of algorithms is the formal derivation and proof,and loop invariant is the key to deriving and proving algorithms formally. But the development of loop invariant is always the most difficult,the most creative and the most challenging issue. This paper studies several typical methods of the existing loop invariant development technology,points out  their basic principles,methods,characteristics and effect. This paper analyses several loop invariant development technologies,and points out some problems,to explore the essential characteristics of loop invariant,thus try to give the research guidance for simple and effective methods.

Key words: loop invariant;PAR method;highreliability software;predict abstract