覆盖所有基础：基于类型的测试输入生成器验证
摘要：测试输入生成器是基于属性的测试（property-based testing，PBT）框架的重要组成部分。由于PBT旨在测试程序的深层语义和结构属性，这些生成器产生的输出可以是复杂的数据结构，并受到开发人员认为与测试所需函数最相关的属性的限制。这些生成器所期望的一个重要特性是能够产生满足函数输入类型和生成器提供的约束条件的所有可接受元素。然而，如何验证特定生成器的输出是否满足这种覆盖要求并不明显。通常，开发人员必须依赖手动检查和事后分析测试运行结果来确定生成器是否提供了足够的覆盖率；这些方法容易出错，并且随着生成器变得更加复杂，很难扩展。为了解决这个重要问题，我们提出了一种基于细化类型的验证过程，用于验证输入测试生成器提供的覆盖范围。该方法基于对类型的新颖解释，将“必须式”欠逼近推理原则嵌入类型系统作为其基本部分。表达式关联的类型现在捕获了表达式保证产生的值的集合，而不是通常使用类型来表示表达式可能产生的值的集合。除了在具有高阶过程和归纳数据类型的丰富核心语言的背景下形式化覆盖类型的概念之外，我们还展示了一个详细的评估研究，以证明我们的想法的实用性。
作者：Zhe Zhou, Ashish Mishra, Benjamin Delaware, Suresh Jagannathan
论文ID：2304.03393
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-11