Detecting Redundant Preconditions

Software specifications often come in the form of contracts, detailing in particular pre- and postconditions of functions, libraries or modules. Research on contracts often centers around questions of contract inference or contract validation. In this paper, we study the less investigated aspect of quality of contracts. More specifically, we define the concept of redundancy for preconditions and propose three techniques with differing efficiency and effectiveness for detecting redundant preconditions. All three techniques are implemented within a software verification tool, and we present results of an experimental evaluation on a dataset of more than 60 C programs. The results confirm differences in precision and resource consumption of the techniques but also reveal unexpected outcomes about the completeness of the most precise, predicate analysis based technique.