一句话:提出枚举组合子的公平性理论,设计公平组合子并证明其性质,用于属性测试更高效地发现程序语言模型缺陷。
属性测试常把枚举表示为自然数与类型元素间的双射,但不同枚举组合子的效率差异很大。本文提出“公平性”性质来刻画更适合属性测试的组合子:公平组合子在构造结果时均衡地索引其参数枚举,例如三元组取第 n 个元素时约向各分量索引 n 的三次方根,三路联合则约返回第 n/3 个元素。作者给出枚举组合子的语义和公平性理论,证明新组合子公平,且某些公平组合子的组合并不公平。最后在寻找编程语言模型缺陷的任务上评估,发现公平枚举组合子与调优随机生成器优势互补(短时间更好、长时间更差),而不公平组合子整体更差。
Abstract Enumerations represented as bijections between the natural numbers and elements of some given type have recently garnered interest in property-based testing because of their efficiency and flexibility. There are, however, many ways of defining these bijections, some of which are better than others. This paper offers a new property of enumeration combinators called fairness that identifies enumeration combinators that are better suited to property-based testing. Intuitively, the result of a fair combinator indexes into its argument enumerations equally when constructing its result. For example, extracting the n th element from our enumeration of three-tuples indexes about $\sqrt[3]{n}$ elements into each of its components instead of, say, indexing $\sqrt[2]{n}$ into one and $\sqrt[4]{n}$ into the other two, as you would if a three-tuple were built out of nested pairs. Similarly, extracting the n th element from our enumeration of a three-way union returns an element that is $\frac{n}{3}$ into one of the argument enumerators. The paper presents a semantics of enumeration combinators, a theory of fairness, proofs establishing fairness of our new combinators and that some combinations of fair combinators are not fair. We also report on an evaluation of fairness for the purpose of finding bugs in programming-language models. We show that fair enumeration combinators have complementary strengths to an existing, well-tuned ad hoc random generator (better on short time scales and worse on long time scales) and that using unfair combinators is worse across the board.