一种证明代码重构后程序正确性的方法
“代码重构”后的程序，可能因为重构编码过程中引入了一些错误而无法正确实现原程序功能，所以需要对其正确性进行验证。但是目前直接证明程序正确性仍难以实现，提出将程序正确性证明转化为程序等价性证明的观点，并提出采用基于合成方法的定理证明技术证明程序等价。该方法避开了直接证明程序正确性的困难，同时也能充分利用现有的定理证明工具，提高了证明的自动化水平，降低了证明的难度。介绍了该方法的原理、基本假设，证明步骤及证明环境，总结了形式化描述中的关键策略，最后采用 RC4算法验证了该方法，实验结果表明了该方法的有效性。
代码重构 程序等价 程序正确性
罗婷 郭渊博 郝耀辉 李虎
中国人民解放军信息工程大学电子技术学院，河南 郑州 450004 中国人民解放军69052 部队，新疆 乌鲁木齐 830000
国内会议
第四届中国计算机网络与信息安全学术会议(CCNIS2011)
郑州
中文
1-5
2011-11-01（万方平台首次上网日期，不代表论文的发表时间）