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

摘要

A lot of progress has been made towards reverse-engineering program specification under the form of contracts. Ensuring the quality of such reverse-engineered contracts, referred to as likely invariants when using 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 which help the user control in two different ways how many variables of the program are considered by Daikon when inferring likely invariants. We perform a case study with a program equipped with test cases and high-level design contracts (i.e., design contracts produced before implementation) and systematically compare likely invariants reverse-engineered by Daikon to those contracts, thanks to a comparison framework we devised. Results confirm and complement previous works, whereby we show that: a good proportion of design contracts are correctly identified by Daikon as likely invariants, many design contracts are not discovered by Daikon, looking for design contract in the set of likely invariants amounts to searching for a needle in a haystack. Our experiment also allows us to suggest a cost-effective configuration when running Daikon.