Test input generators are an important part of property-based testing (PBT) frameworks. Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by these generators can be complex data structures, constrained to satisfy properties the developer believes is most relevant to testing the function of interest. An important feature expected of these generators is that they be capable of producing all acceptable elements that satisfy the function's input type and generator-provided constraints. However, it is not readily apparent how we might validate whether a particular generator's output satisfies this coverage requirement. Typically, developers must rely on manual inspection and post-mortem analysis of test runs to determine if the generator is providing sufficient coverage; these approaches are error-prone and difficult to scale as generators become more complex. To address this important concern, we present a new refinement type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds ``must-style'' underapproximate reasoning principles as a fundamental part of the type system. The types associated with expressions now capture the set of values guaranteed to be produced by the expression, rather than the typical formulation that uses types to represent the set of values an expression may produce. Beyond formalizing the notion of coverage types in the context of a rich core language with higher-order procedures and inductive datatypes, we also present a detailed evaluation study to justify the utility of our ideas.
翻译:测试输入生成器是属性化测试框架(PBT)中的重要部分。因为PBT旨在测试程序的深层语义和结构属性,所以这些生成器产生的输出可以是复杂的数据结构,并受到开发人员认为对测试所关注的函数最相关的属性的限制。这些生成器期望的一个重要特征是,它们能够产生符合函数输入类型和生成器提供的约束的所有可接受元素。然而,我们如何验证特定生成器的输出是否满足此覆盖要求尚不清楚。通常,开发人员必须依靠手动检查和事后分析测试运行结果来确定生成器是否提供足够的覆盖。这些方法容易出错,难以扩展,特别是在生成器变得更加复杂时。为了解决这个重要问题,我们提出了一种新的基于细化类型的验证程序,用于验证测试输入生成器提供的覆盖范围,基于类型的解释嵌入“必须式”欠近似推理原则作为类型系统的基本部分。现在,与表达式相关联的类型捕获所保证的值的集合,而不是使用类型来表示表达式可能产生的值的集合的典型公式。除了在具有高阶过程和归纳数据类型的丰富核心语言的上下文中形式化覆盖类型的概念外,我们还提供了详细的评估研究,以证明我们的想法的实用性。