×

Tests and proofs for custom data generators. (English) Zbl 1425.68373

Summary: We address automated testing and interactive proving of properties involving complex data structures with constraints, like the ones studied in enumerative combinatorics, e.g., permutations and maps. In this paper we show testing techniques to check properties of custom data generators for these structures. We focus on random property-based testing and bounded exhaustive testing, to find counterexamples for false conjectures in the Coq proof assistant. For random testing we rely on the existing Coq plugin QuickChick and its toolbox to write random generators. For bounded exhaustive testing, we use logic programming to generate all the data up to a given size. We also propose an extension of QuickChick with bounded exhaustive testing based on generators developed inside Coq, but also on correct-by-construction generators developed with Why3. These tools are applied to an original Coq formalization of the combinatorial structures of permutations and rooted maps, together with some operations on them and properties about them. Recursive generators are defined for each combinatorial family. They are used for debugging properties which are finally proved in Coq. This large case study is also a contribution in enumerative combinatorics.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68P05 Data structures
PDF BibTeX XML Cite
Full Text: DOI HAL

References:

[1] Baril, J-L, Gray code for permutations with a fixed number of cycles, Discrete Math, 307, 1559-1571, (2007) · Zbl 1128.90039
[2] Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, New York
[3] Bowles J, Caminati MB (2017) A verified algorithm enumerating event structures. In: Intelligent Computer Mathematics, volume 10383 of LNCS (LNAI). Springer, pp 239-254 · Zbl 1367.68245
[4] François B, Sylvain C, Evelyne C, Stéphane L (2008) Implementing polymorphism in SMT solvers. In: SMT ’08/BPR ’08: proceedings of the joint workshops of the 6th international workshop on satisfiability modulo theories and 1st international workshop on bit-precise reasoning. ACM, New York, pp 1-5
[5] Brun, C.; Dufourd, J-F; Magaud, N., Designing and proving correct a convex hull algorithm with hypermaps in Coq, Comput Geom, 45, 436-457, (2012) · Zbl 1247.65021
[6] Bereg, S.; Levy, A.; Sudborough, IH, Constructing permutation arrays from groups, Des Codes Cryptogr, 86, 1095-1111, (2018) · Zbl 1396.05003
[7] Berghofer S, Nipkow T (2004) Random testing in Isabelle/HOL. In: Software engineering and formal methods (SEFM 2004). IEEE Computer Society, pp 230-239
[8] Blanchette, Jasmin Christian; Nipkow, Tobias, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, 131-146, (2010), Berlin, Heidelberg · Zbl 1291.68326
[9] Bulwahn, Lukas, The New Quickcheck for Isabelle, 92-108, (2012), Berlin, Heidelberg · Zbl 1383.68071
[10] Baril, J-L; Vajnovszki, V., A permutation code preserving a double Eulerian bistatistic, Discrete Appl Math, 224, 9-15, (2017) · Zbl 1361.05003
[11] Cruanes, Simon; Blanchette, Jasmin Christian, Extending Nunchaku to Dependent Type Theory, Electronic Proceedings in Theoretical Computer Science, 210, 3-12, (2016)
[12] Carlier M, Dubois C, Gotlieb A (2010) Constraint reasoning in FOCALTEST. In: Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT. SciTePress, pp 82-91
[13] Claessen, Koen; Hughes, John, QuickCheck, ACM SIGPLAN Notices, 35, 268-279, (2000)
[14] Cohen, Cyril, Pragmatic Quotient Types in Coq, 213-228, (2013), Berlin, Heidelberg · Zbl 1317.68207
[15] The Coq Development Team (2017) The Coq Proof Assistant Reference Manual. http://coq.inria.fr/. Version 8.7
[16] Cruanes S (2017) Satisfiability modulo bounded checking. In: Automated deduction-CADE 26, volume 10395 of LNCS. Springer, pp 114-129 · Zbl 06778400
[17] Dubois C, Giorgetti A, Genestier R (2016) Tests and proofs for enumerative combinatorics. In: Tests and proofs (TAP), volume 6792 of LNCS. Springer, pp 57-75 · Zbl 1348.68217
[18] Dybjer, Peter; Haiyan, Qiao; Takeyama, Makoto, Combining Testing and Proving in Dependent Type Theory, 188-203, (2003), Berlin, Heidelberg
[19] Duregård, Jonas; Jansson, Patrik; Wang, Meng, Feat, ACM SIGPLAN Notices, 47, 61, (2013)
[20] Dubois, C.; Mota, J-M, Geometric modeling with B: formal specification of generalized maps., J Sci Pract Comput, 1, 9-24, (2007)
[21] Dufourd, J-F, Design and formal proof of a new optimal image segmentation program with hypermaps, Pattern Recogn, 40, 2974-2993, (2007) · Zbl 1118.68725
[22] Dufourd, J-F, Polyhedra genus theorem and Euler formula: a hypermap-formalized intuitionistic proof, Theor Comput Sci, 403, 133-159, (2008) · Zbl 1154.68100
[23] Dufourd, J-F, An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps., J Autom Reason, 43, 19-51, (2009) · Zbl 1187.68525
[24] Dumont D, Viennot G (1980) A combinatorial interpretation of the Seidel generation of Genocchi numbers. In: Srivastava J (ed) Combinatorial mathematics, optimal designs and their applications, volume 6 of annals of discrete mathematics. Elsevier, pp 77-87 · Zbl 0449.10011
[25] Eynard, B., Formal Matrix Integrals and Combinatorics of Maps, 415-442, (2011), New York, NY · Zbl 1257.81052
[26] Filliâtre J-C, Paskevich A (2013) Why3—where programs meet provers. In: Proceedings of the 22nd European symposium on programming, volume 7792 of LNCS. Springer, pp 125-128
[27] Filliâtre J-C, Pereira M (2016) A modular way to reason about iteration. In: 8th NASA formal methods symposium, volume 9690 of LNCS. Springer, pp 322-336
[28] Genestier, Richard; Giorgetti, Alain; Petiot, Guillaume, Sequential Generation of Structured Arrays and Its Deductive Verification, 109-128, (2015), Cham
[29] Gonthier G (2005) A computer checked proof of the Four Colour Theorem. http://research.microsoft.com/gonthier/4colproof.pdf
[30] Gonthier G (2008) The four colour theorem: engineering of a formal proof. In: ASCM 2007, volume 5081 of LNCS (LNAI). Springer, Heidelberg, pp 333-333 · Zbl 1166.68346
[31] Giorgetti A, Senni V (2012) Specification and validation of algorithms generating planar Lehman words. GASCom’12. https://hal.inria.fr/hal-00753008
[32] Hriţcu C, Lampropoulos L, Dénès M, Paraskevopoulou Z (2018) QuickChick: randomized property-based testing plugin for Coq. https://github.com/QuickChick/QuickChick
[33] Kitaev S (2011) Patterns in permutations and words. Springer, New York · Zbl 1257.68007
[34] Lazarus F (2014) Combinatorial graphs and surfaces from the computational and topological viewpoint followed by some notes on the isometric embedding of the square flat torus. http://www.gipsa-lab.grenoble-inp.fr/ francis.lazarus/Documents/hdr-Lazarus.pdf.
[35] Lehmer DH (1960) Teaching combinatorial tricks to a computer. In: Proceedings of symposia in applied mathematics combinatorial analysis. American Mathematical Society, vol 10, pp 179-193
[36] Lampropoulos L, Gallois-Wong D, Hriţcu C, Hughes J, Pierce BC, Xia L (2017) Beginner’s luck: a language for property-based generators. In: Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, POPL 2017, Paris, France, January 18-20, 2017. ACM, pp 114-129 · Zbl 1380.68096
[37] Lindblad F (2007) Property directed generation of first-order test data. In: Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, New York, USA, April 2-4, 2007, volume 8 of Trends in Functional Programming. Intellect, pp 105-123
[38] Lampropoulos, Leonidas; Paraskevopoulou, Zoe; Pierce, Benjamin C., Generating good generators for inductive relations, Proceedings of the ACM on Programming Languages, 2, 1-30, (2017)
[39] Lando SK, Zvonkin AK (2004) Graphs on surfaces and their applications. Springer
[40] Mathematical Components Team (2018) Mathematical components library. http://math-comp.github.io/math-comp/
[41] Mednykh, A.; Nedela, R., Recent progress in enumeration of hypermaps., J Math Sci, 226, 635-654, (2017) · Zbl 1481.05037
[42] Mantaci, R.; Rakotondrajao, F., A permutations representation that knows what “Eulerian” means, Discrete Math Theor Comput Sci, 4, 101-108, (2001) · Zbl 0965.05002
[43] The OEIS Foundation Inc. The on-line encyclopedia of integer sequences. https://oeis.org/A000698
[44] Owre S (2006) Random testing in PVS. Workshop on Automated Formal Methods (AFM). http://fm.csl.sri.com/AFM06/papers/5-Owre.pdf
[45] Palka MH, Claessen K, Russo A, Hughes J (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. ACM, pp 91-97
[46] Planat, M.; Giorgetti, A.; Holweck, F.; Saniga, M., Quantum contextual finite geometries from dessins d’enfants, Int J Geom Methods Mod Phys, 12, 1-17, (2015) · Zbl 1327.11042
[47] Paraskevopoulou, Zoe; Hriţcu, Cătălin; Dénès, Maxime; Lampropoulos, Leonidas; Pierce, Benjamin C., Foundational Property-Based Testing, 325-343, (2015), Cham · Zbl 1465.68050
[48] Runciman C, Naylor M, Lindblad F (2008) SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. In: Proceedings of the 1st ACM SIGPLAN symposium on Haskell, Haskell 2008, Victoria, BC, Canada, 25 September 2008, pp 37-48
[49] Senni V (2018) Validation library. https://subversion.assembla.com/svn/validation/
[50] Stanley RP (1997) Enumerative combinatorics, vol 1. Cambridge University Press, Cambridge
[51] Seidel, Eric L.; Vazou, Niki; Jhala, Ranjit, Type Targeted Testing, 812-836, (2015), Berlin, Heidelberg
[52] SWI (2018) Prolog. http://www.swi-prolog.org/
[53] Tarau P (2015) On type-directed generation of lambda terms. In: Proceedings of the technical communications of the 31st international conference on logic programming (ICLP 2015), Cork, Ireland, August 31-September 4, 2015, volume 1433 of CEUR Workshop Proceedings. CEUR-WS.org · Zbl 1417.68028
[54] Tutte WT (1973) What is a map? In: New directions in the theory of graphs: proceedings. Academic Press, New York, pp 309-325
[55] Tutte, WT, Combinatorial oriented maps., Can J Math, 31, 986-1004, (1979) · Zbl 0422.05031
[56] Vajnovszki, V., A new Euler-Mahonian constructive bijection., Discrete Appl Math, 159, 1453-1459, (2011) · Zbl 1233.05040
[57] Vajnovszki, V., Lehmer code transforms and Mahonian statistics on permutations., Discrete Math, 313, 581-589, (2013) · Zbl 1259.05006
[58] Walsh, TRS; Lehman, AB, Counting rooted maps by genus I., J Comb Theory Ser B, 13, 192-218, (1972) · Zbl 0228.05108
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.