数值约束的代数递归类型的随机生成器的自动合成
摘要：在程序验证中，基于约束的随机测试是一种强大的技术，旨在生成满足程序功能性属性的随机测试用例。然而，在递归约束数据结构（例如排序列表、二叉搜索树、四叉树）以及结构高度受限时，生成均匀分布的输入是困难的。本文中，我们提出了Testify：一个框架，用户可以定义带有高级约束的代数数据类型。这些约束被解释为限制类型的成员谓词。根据这些定义，Testify自动生成程序的部分规范，以确保没有函数生成违反约束的值（例如，节点被错误地插入的二叉搜索树）。我们的框架为原始程序增加了检查此类属性的测试。为此，我们自动产生均匀随机抽样器来生成满足约束的值，并验证被测试函数的输出的有效性。通过使用Boltzmann抽样生成递归数据结构的形状，并使用约束求解生成均匀分布的有限域变量值，我们的框架保证了大小受限的测试用例的均匀抽样。我们提供了我们的框架在几个对开发人员具有实际意义的关键数据结构上的用例。实验结果显示了令人鼓舞的结果。
作者：Ghiles Ziat, Vincent Botbol, Matthieu Dien, Arnaud Gotlieb, Martin P''epin, Catherine Dubois
论文ID：2208.12747
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-08-29