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旨在测试程序的深层语义和结构属性,所以这些生成器产生的输出可以是复杂的数据结构,并受到开发人员认为对测试所关注的函数最相关的属性的限制。这些生成器期望的一个重要特征是,它们能够产生符合函数输入类型和生成器提供的约束的所有可接受元素。然而,我们如何验证特定生成器的输出是否满足此覆盖要求尚不清楚。通常,开发人员必须依靠手动检查和事后分析测试运行结果来确定生成器是否提供足够的覆盖。这些方法容易出错,难以扩展,特别是在生成器变得更加复杂时。为了解决这个重要问题,我们提出了一种新的基于细化类型的验证程序,用于验证测试输入生成器提供的覆盖范围,基于类型的解释嵌入“必须式”欠近似推理原则作为类型系统的基本部分。现在,与表达式相关联的类型捕获所保证的值的集合,而不是使用类型来表示表达式可能产生的值的集合的典型公式。除了在具有高阶过程和归纳数据类型的丰富核心语言的上下文中形式化覆盖类型的概念外,我们还提供了详细的评估研究,以证明我们的想法的实用性。

0
下载
关闭预览

相关内容

生成器是一次生成一个值的特殊类型函数。可以将其视为可恢复函数。调用该函数将返回一个可用于生成连续 x 值的生成【Generator】,简单的说就是在函数的执行过程中,yield语句会把你需要的值返回给调用生成器的地方,然后退出函数,下一次调用生成器函数的时候又从上次中断的地方开始执行,而生成器内的所有变量参数都会被保存下来供下一次使用。
49篇ICLR2020高分「图机器学习GML」接受论文及代码
专知会员服务
61+阅读 · 2020年1月18日
论文浅尝 | Neural-Symbolic Models for Logical Queries on KG
开放知识图谱
0+阅读 · 2022年10月31日
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
一文带你浏览Graph Transformers
极市平台
1+阅读 · 2022年7月12日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
R工程化—Rest API 之plumber包
R语言中文社区
11+阅读 · 2018年12月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
MoCoGAN 分解运动和内容的视频生成
CreateAMind
18+阅读 · 2017年10月21日
Generative Adversarial Text to Image Synthesis论文解读
统计学习与视觉计算组
13+阅读 · 2017年6月9日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
Towards Reasoning in Large Language Models: A Survey
Arxiv
0+阅读 · 2023年5月26日
Knowledge Embedding Based Graph Convolutional Network
Arxiv
24+阅读 · 2021年4月23日
Arxiv
12+阅读 · 2019年3月14日
VIP会员
相关VIP内容
49篇ICLR2020高分「图机器学习GML」接受论文及代码
专知会员服务
61+阅读 · 2020年1月18日
相关资讯
论文浅尝 | Neural-Symbolic Models for Logical Queries on KG
开放知识图谱
0+阅读 · 2022年10月31日
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
一文带你浏览Graph Transformers
极市平台
1+阅读 · 2022年7月12日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
R工程化—Rest API 之plumber包
R语言中文社区
11+阅读 · 2018年12月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
MoCoGAN 分解运动和内容的视频生成
CreateAMind
18+阅读 · 2017年10月21日
Generative Adversarial Text to Image Synthesis论文解读
统计学习与视觉计算组
13+阅读 · 2017年6月9日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
Top
微信扫码咨询专知VIP会员