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语言中的契约式设计特性，并基于“可满足性模理论”（SMT）的现代程序证明工具的反例生成功能，发展了这种互补性。反例是导致程序失败的输入组合。当我们试图证明程序正确时，我们希望找不到任何反例。然而，我们可以将反例生成应用于错误程序，作为自动测试生成工具。我们还可以向正确程序中引入故障，并将反例转化为具有完全覆盖率的自动生成的回归测试套件。此外，我们可以利用这些机制帮助为错误程序生成修复方案，并保证修复的正确性。这三种应用均基于Eiffel语言和契约式设计的机制，有望显著应对程序测试、软件维护和自动程序修复领域的一些挑战。