Where do contracts - specification elements embedded in executable code - come from? To produce them, should we rely on the programmers, on automatic tools, or some combination?

Recent work, in particular the Daikon system, has shown that it is possible to infer some contracts automatically from program executions. The main incentive has been an assumption that most programmers are reluctant to invent the contracts themselves. The experience of contract-supporting languages, notably Eiffel, disproves that assumption: programmers will include contracts if given the right tools. That experience also shows, however, that the resulting contracts are generally partial and occasionally incorrect.

Contract inference tools provide the opportunity for studying objectively the quality of programmer-written contracts, and for assessing the respective roles of humans and tools. Working on 25 classes taken from different sources such as widely-used standard libraries and code written by students, we applied Daikon to infer contracts and compared the results (totaling more than 19500 inferred assertion clauses) with the already present contracts.

We found that a contract inference tool can be used to strengthen programmer-written contracts, but cannot infer all contracts that humans write. The tool generates around five times as many relevant assertion clauses as written by programmers; but it only finds around 60% of those originally written by programmers. Around a third of the generated assertions clauses are either incorrect or irrelevant. The study also uncovered interesting correlations between the quality of inferred contracts and some code metrics.