循环不变式开发技术研究

作     者：万松松 薛锦云 谢武平 WAN Song-song;XUE Jin-yun;XIE Wu-ping

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

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

出 版 物：《计算机工程与科学》 (Computer Engineering & Science)

年 卷 期：2010年第32卷第9期

页      码：84-88,94页

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

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

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1007-130X.2010.09.023

馆 藏 号：203136395...