Property-Based Testing by Elaborating Proof Outlines

TL;DR

This paper introduces a proof-theoretical framework for property-based testing (PBT) that encodes test generation strategies as proof certificates, enabling systematic and extensible testing of relational specifications, including those with bindings and linear logic.

Contribution

It presents a novel proof-theoretical reconstruction of PBT using proof certificates, extending to complex data structures and linear logic specifications.

Findings

Proof certificates can describe various test generation strategies.

The approach handles data structures with bindings using λ-tree syntax.

Extends PBT to linear logic specifications.

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 $\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).