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 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 : Friday, November 22, 2019 - 5:02:13 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

38

Files downloads

86