Contract systems, especially of the higher-order flavor, go hand in hand with blame. The pragmatic purpose of blame is to narrow down the code that a programmer needs to examine to locate the bug when the contract system discovers a contract violation.
Or so the literature on higher-order contracts claims.
In reality, however, there is neither empirical nor theoretical evidence that connects blame with the location of bugs. The reputation of blame as a tool for weeding out bugs rests on anecdotes about how programmers use contracts to shift blame and their attention from one part of a program to another until they discover the source of the problem.
This paper aims to fill the apparent gap and shed light to the relation between blame and bugs. To that end, we introduce an empirical methodology for investigating whether, for a contract system, it is possible to translate blame information to the location of bugs in a systematic manner. Our methodology is inspired by how programmers attempt to increase the precision of the contracts of a blamed component in order to shift blame to another component, which becomes the next candidate for containing the bug. In particular, we construct a framework that enables us to ask for a contract system whether (i) the process of blame shifting leads blame to settle eventually to the component that contains the bug; and (ii) every shift moves blame “closer” to the faulty component.
Hence our methodology offers a rigorous means for evaluating the pragmatics of contract systems, and we employ it to analyze Racket’s contract system. Along the way, we uncover subtle points about the pragmatic meaning of contracts and blame in Racket: (i) the expressiveness of Racket’s off-the-shelf contract language is not sufficient to narrow down the blamed portion of the code to the faulty component in all cases; and (ii) Racket contracts interfere with program evaluation in subtle ways and thus blame shifting can lead programmers on a detour when searching for a bug.
Conference DayWed 22 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
|What is Decidable about Gradual Types?|
Zeina MigeedUniversity of California, Los Angeles, Jens PalsbergUniversity of California, Los AngelesLink to publication DOI Media Attached File Attached
|Graduality and Parametricity: Together Again for the First Time|
Max NewNortheastern University, Dustin JamnerNortheastern University, USA, Amal AhmedNortheastern University, USALink to publication DOI Media Attached
|Does Blame Shifting Work?|
Lukas LazarekNorthwestern University, Alexis KingNorthwestern University, Samanvitha SundarNorthwestern University, Robby FindlerNorthwestern University, USA, Christos DimoulasPLT @ Northwestern UniversityLink to publication DOI Media Attached