Combining Tests and Proofs with Contracts for Better Software Verification

Abstract

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. Moving past the traditional opposition between tests and proofs, current work on software verification treats them as complementary.