Correct blame for contracts

Abstract

Behavioral software contracts supplement interface information with logical assertions. A rigorous enforcement of contracts provides useful feedback to developers if it signals contract violations as soon as they occur and if it assigns blame to violators with preciseexplanations. Correct blame assignment gets programmers started with the debugging process and can significantly decrease the time needed to discover and fix bugs. Sadly the literature on contracts lacks a framework for making statements about the correctness of blame assignment and for validating such statements. This paper fills the gap and uses the framework to demonstrate how one of the proposed semantics for higher-order contracts satisfies this criteria and another semantics occasionally assigns blame to the wrong module. Concretely, the paper applies the framework to the lax enforcement of dependent higher-order contracts and the picky one. A higher-order dependent contract specifies constraints for the domain and range of higher-order functions and also relates arguments and results in auxiliary assertions. The picky semantics ensures that the use of arguments in the auxiliary assertion satisfies the domain contracts and the lax one does not. While the picky semantics discovers more contract violations than the lax one, it occasionally blames the wrong module. Hence the paper also introduces a third semantics, dubbed indy , which fixes the problems of the picky semantics without giving up its advantages.