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旨在检验程序的深层语义与结构属性，这些生成器产生的输出可能是复杂的数据结构，且需满足开发者认为与测试目标函数最相关的约束条件。对这些生成器的一个关键期望是，它们应当能够生成所有满足函数输入类型和生成器约束条件的合法元素。然而，如何验证特定生成器的输出是否满足这一覆盖要求并非显而易见。通常，开发者需依赖人工检查与测试运行的事后分析来判断生成器是否提供足够覆盖；随着生成器日益复杂，这些方法易出错且难以扩展。为解决这一重要问题，我们提出了一种新的基于精化类型的验证过程，用于验证输入测试生成器提供的覆盖能力。该方法基于一种新颖的类型解释，将“必须风格”的下近似推理原则作为类型系统的基本组成部分。与通常用类型表示表达式可能产生的值集不同，现在与表达式关联的类型捕获了该表达式保证产生的值集。除了在包含高阶过程和归纳数据类型丰富核心语言中形式化覆盖类型的概念外，我们还通过详细的评估研究验证了所提思想的实用性。