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