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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 metadatas

Cited literature [59 references]  Display  Hide  Download

https://hal.inria.fr/hal-02368931
Contributor : Dale Miller <>
Submitted on : Tuesday, November 19, 2019 - 11:43:21 AM
Last modification on : Thursday, March 5, 2020 - 7:07:10 PM
Document(s) archivé(s) le : Thursday, February 20, 2020 - 3:17:46 PM

File

ppdp2019-pbt.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

61

Files downloads

138