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.
Wed 22 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
|What is Decidable about Gradual Types?|
Zeina Migeed University of California, Los Angeles, Jens Palsberg University of California, Los AngelesLink to publication DOI Media Attached File Attached
|Graduality and Parametricity: Together Again for the First Time|
Max New Northeastern University, Dustin Jamner Northeastern University, USA, Amal Ahmed Northeastern University, USALink to publication DOI Media Attached
|Does Blame Shifting Work?|
Lukas Lazarek Northwestern University, Alexis King Northwestern University, Samanvitha Sundar Northwestern University, Robby Findler Northwestern University, USA, Christos Dimoulas PLT @ Northwestern UniversityLink to publication DOI Media Attached