一句话:提出经验方法评估契约系统中归责信息能否系统定位缺陷,并用其分析 Racket 契约系统。
高阶契约系统通常与归责(blame)相伴,其实际目的是在发现契约违反时缩小程序员需要检查的代码范围,从而定位缺陷。然而,归责与缺陷位置之间既缺乏经验证据,也缺乏理论证据。本文受程序员通过细化被归责组件的契约来转移归责、寻找下一候选缺陷组件的做法启发,构建了一个经验框架,用于考察给定契约系统是否满足两点:(i) 归责转移过程最终是否稳定到包含缺陷的组件;(ii) 每次转移是否使归责更接近故障组件。作者用该框架分析 Racket 的契约系统,发现 Racket 现成契约语言的表达力不足以在所有情况下把被归责代码缩小到故障组件;并且,触发状态变化的契约会以微妙方式干扰程序求值,使归责转移把程序员带偏。这些发现展示了此类评估如何为语言设计提供修复方向。
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 given 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 causes blame to eventually settle to the component that contains the bug; and (ii) every shift moves blame ``closer'' to the faulty component. 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) contracts that trigger state changes (even unexpectedly, perhaps in the runtime system's data structures or caches) interfere with program evaluation in subtle ways and thus blame shifting can lead programmers on a detour when searching for a bug. These points highlight how evaluations such as ours suggest fixes to language design.
@article{paperbot516,
title = {Does blame shifting work?},
author = {Lukas Lazarek and Alexis King and Samanvitha Sundar and Robert Bruce Findler and Christos Dimoulas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371133}
}