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