一种证明代码重构后程序正确性的方法

扫码查看

原文链接

NETL

中文摘要：“代码重构”后的程序，可能因为重构编码过程中引入了一些错误而无法正确实现原程序功能，所以需要对其正确性进行验证。但是目前直接证明程序正确性仍难以实现，提出将程序正确性证明转化为程序等价性证明的观点，并提出采用基于合成方法的定理证明技术证明程序等价。该方法避开了直接证明程序正确性的困难，同时也能充分利用现有的定理证明工具，提高了证明的自动化水平，降低了证明的难度。介绍了该方法的原理、基本假设，证明步骤及证明环境，总结了形式化描述中的关键策略，最后采用 RC4算法验证了该方法，实验结果表明了该方法的有效性。

作者：

罗婷、郭渊博、郝耀辉、李虎

展开 >

作者单位：

中国人民解放军信息工程大学电子技术学院，河南郑州 450004

中国人民解放军69052 部队，新疆乌鲁木齐 830000

关键词：

代码重构程序等价程序正确性

主办单位：

中国电子学会

解放军信息工程大学

电子科技大学

会议名称：

第四届中国计算机网络与信息安全学术会议(CCNIS2011)

会议时间：

2011-11-01

会议地点：

郑州

会议母体文献：

第四届中国计算机网络与信息安全学术会议(CCNIS2011)论文集

页码：

1-5

出版时间：

2011