论文标题
失败的证明可以产生有用的测试
A Failed Proof Can Yield a Useful Test
论文作者
论文摘要
在软件验证中，成功的自动化程序证明是最终的胜利。但是，在实践中，这一成功的道路铺平了许多失败的证明尝试。与失败的测试不同，该测试提供了程序中实际错误的具体证据，失败的证明使程序员陷入了黑暗。我们可以从中学到一些有用的东西吗？ 这里报告的工作利用了一些自动抛弃者在尝试证明时收集的有关该程序的丰富内部信息。如果证明失败，则本文介绍的Pirace2-Test工具使用供奉献者生成的反例（具体来说，在AutoProfice System中使用的证明环境Boogie的SMT求解器，用于执行配备合同的EIFFEL程序的正确性证明）来产生失败的测试，为程序员提供了立即可利用的信息来纠正程序以纠正程序。讨论提供了证明2 -Test工具，并演示了思想和工具在代表性示例集中的应用。
A successful automated program proof is, in software verification, the ultimate triumph. In practice, however, the road to such success is paved with many failed proof attempts. Unlike a failed test, which provides concrete evidence of an actual bug in the program, a failed proof leaves the programmer in the dark. Can we instead learn something useful from it? The work reported here takes advantage of the rich internal information that some automatic provers collect about the program when attempting a proof. If the proof fails, the Proof2Test tool presented in this article uses the counterexample generated by the prover (specifically, the SMT solver underlying the proof environment Boogie, used in the AutoProof system to perform correctness proofs of contract-equipped Eiffel programs) to produce a failed test, which provides the programmer with immediately exploitable information to correct the program. The discussion presents the Proof2Test tool and demonstrates the application of the ideas and tool to a collection of representative examples.
