循环不变式开发技术研究

高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。

Analysis of Loop Invariant Development Technology

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.