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

关键词：循环不变式 par方法 高可靠性软件 谓词抽象 

单位：江西师范大学省高性能计算重点实验室 江西南昌330022 江西科技师范学院 江西南昌330013 中国科学院软件研究所计算机科学重点实验室 北京100080