循环不变式开发技术研究  

Analysis of Loop Invariant Development Technology

作　　者：万松松[1,2] 薛锦云[1,3] 谢武平[1] 

机构地区：[1]江西师范大学省高性能计算重点实验室,江西南昌330022 [2]江西科技师范学院,江西南昌330013 [3]中国科学院软件研究所计算机科学重点实验室,北京100080

出　　处：《计算机工程与科学》2010年第9期84-88,94,共6页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(60773054);国家973计划资助项目(2003CCA02800);科技部国际科技合作项目(2008DFA11940)

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

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]