Tests and Proofs: Preface of the Special Issue
Bernhard Beckert and Reiner Hähnle
To prove the correctness of a program is to demonstrate, through
impeccable mathematical techniques, that it has no bugs; to test a
program is to run it with the expectation of discovering bugs. The two
techniques seem contradictory: if you have proved correctness of your
program, it is fruitless to comb it for bugs; and if you are testing
it, that is surely a sign that you have given up any hope to prove its
correctness. Accordingly, proofs and tests have, since the onset of
software engineering research, been pursued by distinct communities
using rather different techniques and tools. And yet the development
of both approaches leads to the discovery of common issues and to the
realization that each may need the other. The emergence of model
checking has been one of the first signs that contradiction may yield
to complementarity, but in the past few years an increasing number of
research efforts have encountered the need for combining proofs and
tests, dropping earlier dogmatic views of incompatibility and taking
instead the best of what each of these software engineering domains
has to offer.
This special issue collects current advances in the ongoing attempt to
obtain synergies from the combination of Tests and Proofs. It arose
from the Second International Conference on Tests and Proofs that took
place in Prato (near Florence), Italy, in April 2008. Our Call for
Papers was addressed to the research community as a whole, but in
addition we invited contributors to the conference to submit revised
versions of their papers, and they have provided two of the five
papers published here. All submissions were refereed to the standard
of an archival journal.