Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: a test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of Design by Contract, as available in Eiffel, and exploiting a feature of modern program-proving tools based on ``Satisfiability Modulo Theories'' (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation. We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and Design by Contract, hold significant promise to address some of the challenges of program testing, software maintenance and Automatic Program Repair.

翻译：测试还是证明？长期以来，这两种软件验证方法常被视为对立。一种是动态的，另一种是静态的：测试执行程序，而证明仅分析程序文本。一种新的视角正在兴起，其中测试与证明被视为实现已验证质量软件的互补技术，而非相互竞争。过去几年开展并在此综述的研究工作，通过利用Eiffel语言中可用的契约式设计，以及基于“可满足性模理论”的现代程序证明工具的一项特性——反例生成，发展了这种互补性。反例是导致程序失败的输入组合。当我们试图证明程序正确时，我们希望找不到任何反例。然而，我们可以将反例生成应用于不正确的程序，作为自动测试生成的工具。我们还可以向正确程序中引入故障，并将反例转化为具有完全覆盖率的自动生成的回归测试套件。此外，我们可以利用这些机制帮助为不正确程序生成程序修复，并保证修复的正确性。这三种应用均基于Eiffel语言和契约式设计的机制，有望显著应对程序测试、软件维护和自动程序修复领域的一些挑战。