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.

翻译：成功的自动化程序证明在软件验证中是终极成就。然而在实践中，通往成功的道路布满无数失败的证明尝试。与失败的测试不同——后者能提供程序中实际错误的具体证据——失败的证明让程序员无所适从。我们能否从中获取有用信息？本文报告的工作利用了某些自动证明器在尝试证明过程中收集的丰富内部信息。当证明失败时，本文介绍的Proof2Test工具利用证明器生成的对抗样例（具体而言，是Boogie证明环境底层使用的SMT求解器——该求解器在AutoProof系统中用于对带契约的Eiffel程序进行正确性证明）生成失败的测试，从而为程序员提供可立即用于修正程序的信息。本文论述了Proof2Test工具，并通过一系列代表性示例演示了相关思想与工具的应用。