Skip to Main content Skip to Navigation
Conference papers

Property-Based Testing via Proof Reconstruction

Roberto Blanco 1 Dale Miller 2 Alberto Momigliano 3 
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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 Foun-dational Proof Certificate framework to describe test generators. We do this by presenting certain kinds of "proof outlines" that can be used to 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 towards their explanation. Once generation is accomplished, the testing phase boils down to a standard logic programming search. After illustrating our techniques on simple, first-order (algebraic) data structures, we lift it to data structures containing bindings using λ-tree syntax. The λProlog programming language is capable of performing both the generation and checking of tests. We validate this approach by tackling benchmarks in the metatheory of programming languages coming from related tools such as PLT-Redex. CCS CONCEPTS • Software and its engineering → Formal software verification; • Theory of computation → Logic and verification; Proof theory.
Complete list of metadata

Cited literature [59 references]  Display  Hide  Download
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Tuesday, November 19, 2019 - 11:43:21 AM
Last modification on : Thursday, June 9, 2022 - 3:41:05 AM
Long-term archiving on: : Thursday, February 20, 2020 - 3:17:46 PM


Files produced by the author(s)



Roberto Blanco, Dale Miller, Alberto Momigliano. Property-Based Testing via Proof Reconstruction. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-13, ⟨10.1145/3354166.3354170⟩. ⟨hal-02368931⟩



Record views


Files downloads