research-article

Property-Based Testing via Proof Reconstruction

Authors:

Roberto Blanco,

Alberto MomiglianoAuthors Info & Claims

PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming

Article No.: 5, Pages 1 - 13

https://doi.org/10.1145/3354166.3354170

Published: 07 October 2019 Publication History

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 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.

References

[1]

Beniamino Accattoli. 2012. Proof pearl: Abella formalization of lambda calculus cube property. In Second International Conference on Certified Programs and Proofs (Lecture Notes in Computer Science), Chris Hawblitzel and Dale Miller (Eds.), Vol. 7679. Springer, 173--187.

Digital Library

[2]

Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. J. of Logic and Computation 2, 3 (1992), 297--347. https://doi.org/10.1093/logcom/2.3.297

[3]

K. R. Apt and M. H. van Emden. 1982. Contributions to the theory of logic programming. JACM 29, 3 (1982), 841--862.

Digital Library

[4]

Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2017. Intrinsically-typed Definitional Interpreters for Imperative Languages. Proc. ACM Program. Lang. 2, POPL, Article 16 (Dec. 2017), 34 pages. http://doi.acm.org/10.1145/3158104

Digital Library

[5]

David Baelde. 2012. Least and greatest fixed points in linear logic. ACM Trans. on Computational Logic 13, 1 (April 2012), 2:1--2.44. https://doi.org/10.1145/2071368.2071370

Digital Library

[6]

David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7, 2 (2014).

[7]

David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. 2007. The Bedwyr system for model checking over syntactic expressions. In 21th Conf. on Automated Deduction (CADE) (LNAI), F. Pfenning (Ed.). Springer, New York, 391--397.

Digital Library

[8]

Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. 2011. Automatic Proof and Disproof in Isabelle/HOL. In FroCoS (Lecture Notes in Computer Science), Cesare Tinelli and Viorica Sofronie-Stokkermans (Eds.), Vol. 6989. Springer, 12--27.

[9]

Roberto Blanco, Zakaria Chihani, and Dale Miller. 2017. Translating Between Implicit and Explicit Versions of Proof. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction (Lecture Notes in Computer Science), Leonardo de Moura (Ed.), Vol. 10395. Springer, 255--273.

[10]

Roberto Blanco and Dale Miller. 2015. Proof Outlines as Proof Certificates: a system description. In Proceedings First International Workshop on Focusing (Electronic Proceedings in Theoretical Computer Science), Iliano Cervesato and Carsten Schürmann (Eds.), Vol. 197. Open Publishing Association, 7--14.

[11]

Luc Bougé, N. Choquet, Laurent Fribourg, and Marie-Claude Gaudel. 1986. Test sets generation from algebraic specifications using logic programming. Journal of Systems and Software 6, 4 (1986), 343--360.

Digital Library

[12]

Lukas Bulwahn. 2012. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. In Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings (Lecture Notes in Computer Science), Chris Hawblitzel and Dale Miller (Eds.), Vol. 7679. Springer, 92--108. https://doi.org/10.1007/978-3-642-35308-6_10

[13]

James Cheney and Alberto Momigliano. 2017. α Check: A mechanized metatheory model checker. Theory and Practice of Logic Programming 17, 3 (2017), 311âĂş352.

[14]

James Cheney, Alberto Momigliano, and Matteo Pessina. 2016. Advances in Property-Based Testing for αProlog. In Tests and Proofs - 10th International Conference, TAP 2016, Vienna, Austria, July 5-7, 2016, Proceedings (Lecture Notes in Computer Science), Bernhard K. Aichernig and Carlo A. Furia (Eds.), Vol. 9762. Springer, 37--56.

[15]

Zakaria Chihani, Dale Miller, and Fabien Renaud. 2017. A semantic framework for proof evidence. J. of Automated Reasoning 59, 3 (2017), 287--330. https://doi.org/10.1007/s10817-016-9380-6

Digital Library

[16]

Koen Claessen, Jonas Duregård, and Michal H. Palka. 2015. Generating constrained random data with uniform distribution. J. Funct. Program. 25 (2015). https://doi.org/10.1017/S0956796815000143

[17]

Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP 2000). ACM, 268--279.

Digital Library

[18]

K. L. Clark. 1978. Negation as failure. In Logic and Data Bases, J. Gallaire and J. Minker (Eds.). Plenum Press, New York, 293--322.

[19]

Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. 2015. ELPI: Fast, Embeddable, λProlog Interpreter. In Proceedings of LPAR. Suva, Fiji. https://hal.inria.fr/hal-01176856

Digital Library

[20]

Jonas Duregård, Patrik Jansson, and Meng Wang. 2012. Feat: functional enumeration of algebraic types. In Haskell Workshop, Janis Voigtländer (Ed.). ACM, 61--72. https://doi.org/10.1145/2364506.2364515

Digital Library

[21]

Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. The MIT Press.

[22]

Amy P. Felty and Alberto Momigliano. 2012. Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax. J. Autom. Reasoning 48, 1 (2012), 43--105. https://doi.org/10.1007/s10817-010-9194-x

Digital Library

[23]

Burke Fetscher, Koen Claessen, Michal H. Palka, John Hughes, and Robert Bruce Findler. 2015. Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System. In ESOP (Lecture Notes in Computer Science), Vol. 9032. Springer, 383--405.

[24]

Daan Fierens, Guy Van den Broeck, Joris Renkens, Dimitar Sht. Shterionov, Bernd Gutmann, Ingo Thon, Gerda Janssens, and Luc De Raedt. 2015. Inference and learning in probabilistic logic programs using weighted Boolean formulas. TPLP 15, 3 (2015), 358--401. https://doi.org/10.1017/S1471068414000076

[25]

Fabio Fioravanti, Maurizio Proietti, and Valerio Senni. 2015. Efficient generation of test data structures using constraint logic programming and program transformation. J. Log. Comput. 25, 6 (2015), 1263--1283. https://doi.org/10.1093/logcom/ext071

[26]

Andrew Gacek, Dale Miller, and Gopalan Nadathur. 2008. Combining generic judgments with recursive definitions. In 23th Symp. on Logic in Computer Science, F. Pfenning (Ed.). IEEE Computer Society Press, 33--44.

Digital Library

[27]

Andrew Gacek, Dale Miller, and Gopalan Nadathur. 2012. A two-level logic approach to reasoning about computations. J. of Automated Reasoning 49, 2 (2012), 241--273. https://doi.org/10.1007/s10817-011-9218-1

Digital Library

[28]

Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science 50, 1 (1987), 1--102. https://doi.org/10.1016/0304-3975(87)90045-4

Digital Library

[29]

Jean-Yves Girard. 1992. A Fixpoint Theorem in Linear Logic. (Feb. 1992). An email posting to the mailing list [email protected].

[30]

Quentin Heath and Dale Miller. 2017. A Proof Theory for Model Checking: An Extended Abstract. In Proceedings Fourth International Workshop on Linearity (LINEARITY 2016) (EPTCS), Iliano Cervesato and Maribel Fernández (Eds.), Vol. 238.

[31]

Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. 2013. Testing Noninterference, Quickly. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP '13). ACM, New York, NY, USA, 455--468. https://doi.org/10.1145/2500365.2500574

Digital Library

[32]

John Hughes. 2007. QuickCheck Testing for Fun and Profit. In Practical Aspects of Declarative Languages, 9th International Symposium, PADL 2007, Nice, France, January 14-15, 2007 (Lecture Notes in Computer Science), Michael Hanus (Ed.), Vol. 4354. Springer, 1--32.

[33]

Andrew Ireland and Alan Bundy. 1996. Productive use of failure in inductive proof. Journal of Automated Reasoning 16 (1996), 79--111.

Digital Library

[34]

Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. 2012. Run your research: on the effectiveness of light weight mechanization. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '12). ACM, New York, NY, USA, 285--296.

Digital Library

[35]

Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. 2017. Beginner's Luck: A Language for Random Generators. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). https://arxiv.org/abs/1607.05443

[36]

Chuck Liang and Dale Miller. 2009. Focusing and Polarization in Linear, Intuitionistic, and Classical Logics. Theoretical Computer Science 410, 46 (2009), 4747--4768.

Digital Library

[37]

Raymond McDowell and Dale Miller. 2000. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science 232 (2000), 91--119. https://doi.org/10.1016/S0304-3975(99)00171-1

Digital Library

[38]

Raymond McDowell and Dale Miller. 2002. Reasoning with Higher-Order Abstract Syntax in a Logical Framework. ACM Trans. on Computational Logic 3, 1 (2002), 80--136.

Digital Library

[39]

Raymond McDowell, Dale Miller, and Catuscia Palamidessi. 2003. Encoding transition systems in sequent calculus. Theoretical Computer Science 294, 3 (2003), 411--437.

Digital Library

[40]

Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson. 2017. Effect-driven QuickChecking of compilers. PACMPL 1, ICFP (2017), 15:1--15.23. https://doi.org/10.1145/3110259

[41]

Dale Miller. 2018. Mechanized Metatheory Revisited. Journal of Automated Reasoning (04 Oct. 2018). https://doi.org/10.1007/s10817-018-9483-3

[42]

Dale Miller and Gopalan Nadathur. 2012. Programming with Higher-Order Logic. Cambridge University Press.

[43]

Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. 1991. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logic 51 (1991), 125--157.

[44]

Dale Miller and Alexis Saurin. 2006. A Game Semantics for Proof Search: Preliminary Results. Electr. Notes Theor. Comput. Sci. 155 (2006), 543--563. https://doi.org/10.1016/j.entcs.2005.11.072

Digital Library

[45]

Dale Miller and Alwen Tiu. 2005. A proof theory for generic judgments. ACM Trans. on Computational Logic 6, 4 (Oct. 2005), 749--783.

Digital Library

[46]

Alberto Momigliano. 2000. Elimination of Negation in a Logical Framework. In CSL (Lecture Notes in Computer Science), Vol. 1862. Springer, 411--426.

[47]

Alberto Momigliano. 2012. A supposedly fun thing i may have to do again: a HOAS encoding of Howe's method. In Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practice (LFMTP '12). ACM, New York, NY, USA, 33--42. http://doi.acm.org/10.1145/2364406.2364411

Digital Library

[48]

Gopalan Nadathur and Frank Pfenning. 1992. The type system of a higher-order logic programming language. In Types in Logic Programming, Frank Pfenning (Ed.). MIT Press, 245--283.

[49]

Roberto Blanco Martínez. 2017. Applications of Foundational Proof Certificates in theorem proving. Ph.D. Dissertation. Université Paris-Saclay.

[50]

Michal H. Palka, Koen Claessen, Alejandro Russo, and John Hughes. 2011. Testing an optimising compiler by generating random lambda terms. In Proceedings of the 6th International Workshop on Automation of Software Test, AST 2011, Waikiki, Honolulu, HI, USA, May 23-24, 2011, Antonia Bertolino, Howard Foster, and J. Jenny Li (Eds.). ACM, 91--97. https://doi.org/10.1145/1982595.1982615

[51]

Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. 2015. Foundational Property-Based Testing. In Interactive Theorem Proving - 6th International Conference, ITP 2015, Proceedings (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, 325--343.

[52]

Giridhar Pemmasani, Hai-Feng Guo, Yifei Dong, C. R. Ramakrishnan, and I. V. Ramakrishnan. 2004. Online Justification for Tabled Logic Programs. In Functional and Logic Programming, Yukiyoshi Kameyama and Peter J. Stuckey (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 24--38.

[53]

Frank Pfenning and Carsten Schürmann. 1999. System Description: Twelf -- A Meta-Logical Framework for Deductive Systems. In 16th Conf. on Automated Deduction (CADE) (LNAI), H. Ganzinger (Ed.). Springer, Trento, 202--206. https://doi.org/10.1007/3-540-48660-7_14

[54]

Brigitte Pientka and Joshua Dunfield. 2010. Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). In Fifth International Joint Conference on Automated Reasoning (Lecture Notes in Computer Science), J. Giesl and R. Hähnle (Eds.). 15--21.

Digital Library

[55]

A. M. Pitts. 1997. Operationally Based Theories of Program Equivalence. In Semantics and Logics of Computation, P. Dybjer and A. M. Pitts (Eds.).

[56]

Colin Runciman, Matthew Naylor, and Fredrik Lindblad. 2008. Smallcheck and Lazy Smallcheck: automatic exhaustive testing for small values. In Haskell. ACM, 37--48.

[57]

Tom Schrijvers, Bart Demoen, Markus Triska, and Benoit Desouter. 2014. Tor: Modular search with hookable disjunction. Sci. Comput. Program. 84 (2014), 101--120. https://doi.org/10.1016/j.scico.2013.05.008

Digital Library

[58]

Peter Schroeder-Heister. 1993. Definitional Reflection and the Completion. In Proceedings of the 4th International Workshop on Extensions of Logic Programming, R. Dyckhoff (Ed.). Springer-Verlag LNAI 798, 333--347.

[59]

Peter Schroeder-Heister. 1993. Rules of Definitional Reflection. In 8th Symp. on Logic in Computer Science, M. Vardi (Ed.). IEEE Computer Society Press, IEEE, 222--232. https://doi.org/10.1109/LICS.1993.287585

[60]

Kevin Sullivan, Jinlin Yang, David Coppit, Sarfraz Khurshid, and Daniel Jackson. 2004. Software Assurance by Bounded Exhaustive Testing. In Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '04). ACM, New York, NY, USA, 133--142. https://doi.org/10.1145/1007512.1007531

Digital Library

[61]

Alwen Tiu and Dale Miller. 2010. Proof Search Specifications of Bisimulation and Modal Logics for the π-calculus. ACM Trans. on Computational Logic 11, 2 (2010), 13:1--13.35. https://doi.org/10.1145/1656242.1656248

Digital Library

Cited By

Momigliano ASassella M(2024)More Church-Rosser Proofs in BELUGAElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.402.6402(34-42)Online publication date: 23-Apr-2024
https://doi.org/10.4204/EPTCS.402.6
Mantovani MMomigliano A(2021)Towards Substructural Property-Based TestingLogic-Based Program Synthesis and Transformation10.1007/978-3-030-98869-2_6(92-112)Online publication date: 7-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-98869-2_6

Index Terms

Property-Based Testing via Proof Reconstruction
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Logic
    1. Logic and verification
    2. Proof theory

Recommendations

Proof search for propositional abstract separation logics via labelled sequents
POPL '14

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called ...
Proof search for propositional abstract separation logics via labelled sequents
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called ...
Model-based mutation testing via symbolic refinement checking

In model-based mutation testing, a test model is mutated for test case generation. The resulting test cases are able to detect whether the faults in the mutated models have been implemented in the system under test. For this purpose, a conformance check ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming

October 2019

280 pages

ISBN:9781450372497

DOI:10.1145/3354166

Program Chair:
Ekaterina Komendantskaya

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

In-Cooperation

Sony: Sony Corporation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 October 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed limited

Conference

PPDP '19

PPDP '19: Principles and Practice of Programming Languages 2019

October 7 - 9, 2019

Porto, Portugal

Acceptance Rates

PPDP '19 Paper Acceptance Rate 19 of 45 submissions, 42%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
99
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)1

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Momigliano ASassella M(2024)More Church-Rosser Proofs in BELUGAElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.402.6402(34-42)Online publication date: 23-Apr-2024
https://doi.org/10.4204/EPTCS.402.6
Mantovani MMomigliano A(2021)Towards Substructural Property-Based TestingLogic-Based Program Synthesis and Transformation10.1007/978-3-030-98869-2_6(92-112)Online publication date: 7-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-98869-2_6

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents