一种基于语境的程序正确性验证算法的研究与实现

摘要：

传统的程序验证方法如Hoare逻辑,最弱前置谓词法,存在中间断言构造困难、依赖于循环不变式、证明复杂等缺点.针对于这些缺点,本文提出基于语境的形式化证明方法,设计了一套基于语境的形式公理系统,将语境的概念和限定数学归纳法引入到程序验证中去,即用语境来记录程序运行环境和上下文,用限定数学归纳法来验证循环结构的程序,避免了循环不变式的构造,简化了验证过程,降低了验证难度。

关键词： 计算机程序 正确性验证 循环不变式 语境 限定数学归纳法

作者: 尹顺顺 马殿富 赵永望 赵宪琦

作者单位: 北京航空航天大学计算机学院 北京 100191

会议类型: 国内会议

会议名称: 全国抗恶劣环境计算机第二十四届学术年会

会议地点: 江西九江

会议语种:中文

页码: 297-304

在线出版日期: 2014-09-01（万方平台首次上网日期，不代表论文的发表时间）