Property-based testing (PBT) is a popular technique for automatically testing semantic properties of a program, specified as a pair of pre- and post-conditions. The efficacy of this approach depends on being able to quickly generate inputs that meet the precondition, in order to maximize the set of program behaviors that are probed. For semantically rich preconditions, purely random generation is unlikely to produce many valid inputs; when this occurs, users are forced to manually write their own specialized input generators. One common problem with handwritten generators is that they may be incomplete, i.e., they are unable to generate some values meeting the target precondition. This paper presents a novel program repair technique that patches an incomplete generator so that its range includes every valid input. Our approach uses a novel enumerative synthesis algorithm that leverages the recently developed notion of coverage types to characterize the set of missing test values as well as the coverage provided by candidate repairs. We have implemented a repair tool for OCaml generators, called Cobb, and used it to repair a suite of benchmarks drawn from the PBT literature.
翻译:基于属性的测试是一种流行的自动化测试技术,用于验证程序语义属性,这些属性通过前置条件和后置条件对来定义。该方法的有效性取决于能否快速生成满足前置条件的输入,从而最大化探测程序行为的范围。对于语义丰富的前置条件,纯随机生成不太可能产生大量有效输入;当出现这种情况时,用户不得不手动编写专门的输入生成器。手写生成器的一个常见问题是它们可能不完整,即无法生成某些满足目标前置条件的值。本文提出了一种新颖的程序修复技术,能够修补不完整的生成器,使其值域包含所有有效输入。我们的方法采用了一种创新的枚举式合成算法,该算法利用最近提出的覆盖类型概念来刻画缺失测试值集合以及候选修复提供的覆盖范围。我们实现了一个名为Cobb的OCaml生成器修复工具,并用其修复了从PBT文献中提取的一系列基准测试用例。