A Comparative Study of Invariants Generated by Daikon and User-Defined Design Contracts

A lot of progress has been made towards the reverse-engineering of program specification under the form of contracts. Ensuring the quality of such reverse-engineered contracts, referred to as likely invariants when one uses Daikon, is paramount since those contracts are used in several other contexts. One aspect that can influence the “quality” of the reverse-engineered contracts is the configuration being used when executing Daikon. In this paper we evaluate the impact of two such configuration parameters. We perform a case study with a program equipped with test cases and high-level design and systematically compare likely invariants reverse-engineered by Daikon to those contracts. Results confirm and complement previous works, whereby we show that a good proportion of contracts are correctly identified by Daikon as likely invariants, and therefore that many interesting contracts are not discovered by Daikon, but these likely invariants are lost in a mass of incorrect ones.