In program verification, constraint-based random testing is a powerful technique which aims at generating random test cases that satisfy functional properties of a program. However, on recursive constrained data-structures (e.g., sorted lists, binary search trees, quadtrees), and, more generally, when the structures are highly constrained, generating uniformly distributed inputs is difficult. In this paper, we present Testify: a framework in which users can define algebraic data-types decorated with high-level constraints. These constraints are interpreted as membership predicates that restrict the set of inhabitants of the type. From these definitions, Testify automatically synthesises a partial specification of the program so that no function produces a value that violates the constraints (e.g. a binary search tree where nodes are improperly inserted). Our framework augments the original program with tests that check such properties. To achieve that, we automatically produce uniform random samplers that generate values which satisfy the constraints, and verifies the validity of the outputs of the tested functions. By generating the shape of a recursive data-structure using Boltzmann sampling and generating evenly distributed finite domain variable values using constraint solving, our framework guarantees size-constrained uniform sampling of test cases. We provide use-cases of our framework on several key data structures that are of practical relevance for developers. Experiments show encouraging results.
翻译:在程序核查中,基于约束的随机测试是一种强大的技术,旨在生成随机测试案例,满足程序功能特性。然而,对于循环约束的数据结构(例如分类列表、二进制搜索树、四叶树),以及更一般地说,当结构高度限制时,很难产生统一分布的输入。在本文件中,我们提出验证:用户可以用来定义代数数据类型的框架,在高层次限制下标注数据类型。这些限制被解释为会籍前提,限制该类居民的组合。根据这些定义,测试自动合成程序的部分规格,以便没有任何功能产生违反限制值(例如,分类列表、二进制搜索树、四叶树),更一般地说,当结构高度限制时,则生成统一分布的分布式数据类型。为了实现这一点,我们自动生成统一的随机抽样样本,从而满足限制,并验证测试函数的正确性。通过这些定义,通过Boltzmann取样和生成均衡分布式的数据结构,从而产生一个违反限制度的值(例如,在节点中插入节点插入一个二进式关键域内值的测试框架),我们使用一些统一的实验性标准。