Property-Based Testing via Proof Reconstruction Work-in-progress

Abstract : Property-based testing is a technique for validating code against an executable specification by automatically generating test-data. From its original use in programming languages, this technique has now spread to most major proof assistants to complement theorem proving with a preliminary phase of conjecture testing. We present a proof theoretical reconstruction of this style of testing for relational specifications (such as those used in the semantics of programming languages) and employ the Foundational Proof Certificate framework to aid in describing test generators. We do this by presenting certain kinds of " proof outlines " that can be used to describe the shape and size of the generators for the conditional part of a proposed property. Then the testing phase is reduced to 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.
Type de document :
Communication dans un congrès
LFMTP 17: Logical Frameworks and Meta-Languages: Theory and Practice, Sep 2017, Oxford, United Kingdom
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01646788
Contributeur : Dale Miller <>
Soumis le : jeudi 23 novembre 2017 - 17:49:43
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01

Fichier

lfmtp17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01646788, version 1

Citation

Roberto Blanco, Dale Miller, Alberto Momigliano. Property-Based Testing via Proof Reconstruction Work-in-progress. LFMTP 17: Logical Frameworks and Meta-Languages: Theory and Practice, Sep 2017, Oxford, United Kingdom. 〈hal-01646788〉

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

32