Correct blame for contracts: No more scapegoating

Christos Dimoulas*, Robert Bruce Findler, Cormac Flanagan, Matthias Felleisen

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

34 Scopus citations

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 precise explanations. 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.

Original languageEnglish (US)
Pages (from-to)215-226
Number of pages12
JournalACM SIGPLAN Notices
Volume46
Issue number1
DOIs
StatePublished - Jan 1 2011

Keywords

  • Behavioral contracts
  • Blame assignment
  • Higher-order programming

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Correct blame for contracts: No more scapegoating'. Together they form a unique fingerprint.

Cite this