一句话:提出基于覆盖类型的枚举合成算法,自动修复不完整的属性测试输入生成器,使其能生成所有满足前置条件的输入。
基于属性的测试(PBT)通过前置/后置条件描述程序语义性质,其有效性依赖于快速生成满足前置条件的输入。当前置条件语义丰富时,纯随机生成难以产生有效输入,用户不得不手写专门的输入生成器,而手写生成器常常是不完整的——无法生成某些满足前置条件的值。本文提出一种新的程序修复技术,能够修补不完整的生成器,使其值域覆盖所有合法输入。其核心是新颖的枚举式合成算法,利用近期提出的「覆盖类型(coverage types)」概念,同时刻画缺失测试值集合以及候选修复所提供的覆盖范围。作者实现了面向 OCaml 生成器的修复工具 Cobb,并在取自 PBT 文献的基准测试集上验证了其修复能力。
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.
@article{paperbot2898,
title = {We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators},
author = {Patrick LaFontaine and Zhe Zhou and Ashish Mishra and Suresh Jagannathan and Benjamin Delaware},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763158}
}