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 $\lambda$-tree syntax approach to encode bindings. The $\lambda$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).

翻译：属性测试是一种通过自动生成测试数据来验证代码是否符合可执行规范的技术。本文针对关系式规范提出了此类测试方法的证明论重构，并采用基础证明证书框架来描述测试生成器。具体而言，我们将特定类型的"证明纲要"编码为可描述PBT文献中各种常见生成策略的证明证书——涵盖从随机生成到穷举生成及其组合策略。同时，我们探讨了反例缩减技术，将其作为解释反例的第一步。生成阶段完成后，测试阶段即转化为标准的逻辑编程搜索过程。在通过简单的一阶（代数）数据结构演示我们的技术后，我们将其提升至包含绑定的数据结构——采用λ树语法方法对绑定进行编码。基于这种语法处理方法，λProlog编程语言能够同时执行测试的生成与验证。随后，我们进一步将属性测试扩展至线性逻辑片段中的规范。本文已投稿至《逻辑编程理论与实践》（TPLP）期刊。