Property-Based Testing by Elaborating Proof Outlines
Dale Miller, Alberto Momigliano
TL;DR
This work presents a unified, logic-based framework for property-based testing (PBT) by separating generation and checking into two levels: a specification logic $SL$ for relational entailment and a reasoning logic $RL$ for inductive proof-theoretic reasoning. Counterexample search is guided by Foundational Proof Certificates (FPC), which describe proof outlines and can express generation strategies from exhaustive to randomized, as well as shrinking of counterexamples. Implemented in $\\lambda$Prolog, the approach supports both first-order Horn clauses and richer meta-programming features, including $\\lambda$-tree syntax for bindings and a fragment of linear logic, enabling test generation and verification in a single framework. The paper demonstrates flexible generation strategies, meta-programming extensions, and counterexample explanations, offering a principled, programmable foundation for PBT with potential integration to existing proof environments. Overall, it provides a proof-theoretic reconstruction of PBT that unifies specification, proof search, and test generation under a two-level logic and certificate-based control flow.
Abstract
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).