基于证明大纲展开的属性测试
Property-Based Testing by Elaborating Proof Outlines
AI总结：
本文提出一种基于证明证书编码证明大纲的属性测试方法，覆盖随机到穷举的生成策略，并支持反例收缩，可扩展到含绑定及线性逻辑规范。
摘要：
属性测试（PBT）是一种通过自动生成测试数据，依据可执行规范来验证代码的技术。我们针对关系型规范提出了这种测试风格的证明论重构，并利用基础证明证书框架来描述测试生成器。我们通过将某些类型的“证明大纲”编码为证明证书来实现这一点，这些证书能够描述PBT文献中各种常见的生成策略，从随机到穷举，包括它们的组合。我们还处理了反例的收缩，作为向解释反例迈出的第一步。一旦生成完成，测试阶段就是标准的逻辑编程搜索。在简单的、一阶（代数）数据结构上演示了我们的技术之后，我们通过使用λ-树语法方法来编码绑定，将其提升到包含绑定的数据结构。λProlog编程语言可以使用这种语法方法同时执行测试的生成和检查。然后，我们进一步将PBT扩展到线性逻辑片段中的规范。本文考虑发表于《逻辑编程理论与实践》（TPLP）。
英文摘要：
Property-based testing (PBT) is a technique for validating code against an executable specification by automatically generating test-data. We present a proof-theoretical reconstruction of this style of testing for relational specifications and employ the Foundational Proof Certificate framework to describe test generators. We do this by encoding certain kinds of ``proof outlines'' as proof certificates that can describe various common generation strategies in the PBT literature, ranging from random to exhaustive, including their combination. We also address the shrinking of counterexamples as a first step toward their explanation. Once generation is accomplished, the testing phase is a standard logic programming search. After illustrating our techniques on simple, first-order (algebraic) data structures, we lift it to data structures containing bindings by using the $λ$-tree syntax approach to encode bindings. The $λ$Prolog programming language can perform both generating and checking of tests using this approach to syntax. We then further extend PBT to specifications in a fragment of linear logic. Under consideration in Theory and Practice of Logic Programming (TPLP).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
