{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T19:40:06Z","timestamp":1751744406350,"version":"3.41.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-018-0459-1","type":"journal-article","created":{"date-parts":[[2018,7,12]],"date-time":"2018-07-12T06:45:34Z","timestamp":1531377934000},"page":"659-684","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Tests and proofs for custom data generators"],"prefix":"10.1145","volume":"30","author":[{"given":"Catherine","family":"Dubois","sequence":"first","affiliation":[{"name":"Samovar, ENSIIE, CNRS, \u00c9vry, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0990-9611","authenticated-orcid":false,"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[{"name":"FEMTO-ST Institute, University of Bourgogne Franche-Comt\u00e9, CNRS, Besan\u00e7on, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2006.09.007"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bertot Y Cast\u00e9ran P (2004) Interactive theorem proving and program development. Coq\u2019Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer New York","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bowles J Caminati MB (2017) A verified algorithm enumerating event structures. In: Intelligent Computer Mathematics volume 10383 of LNCS (LNAI). Springer pp 239\u2013254","DOI":"10.1007\/978-3-319-62075-6_17"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois B Sylvain C Evelyne C St\u00e9phane L (2008) Implementing polymorphism in SMT solvers. In: SMT \u201908\/BPR \u201908: 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\u20135","DOI":"10.1145\/1512464.1512466"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comgeo.2010.06.006"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10623-017-0381-1"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Berghofer S Nipkow T (2004) Random testing in Isabelle\/HOL. In: Software engineering and formal methods (SEFM 2004). IEEE Computer Society pp 230\u2013239","DOI":"10.1109\/SEFM.2004.1347524"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2017.02.014"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.4204\/EPTCS.210.3","article-title":"Extending Nunchaku to Dependent Type Theory","volume":"210","author":"Cruanes Simon","year":"2016","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"e_1_2_1_2_12_2","unstructured":"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\u201391"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351266"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/978-3-642-39634-2_17","volume-title":"Interactive Theorem Proving","author":"Cohen Cyril","year":"2013"},{"key":"e_1_2_1_2_15_2","unstructured":"The Coq Development Team (2017) The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr\/. Version 8.7"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Cruanes S (2017) Satisfiability modulo bounded checking. In: Automated deduction\u2013CADE 26 volume 10395 of LNCS. Springer pp 114\u2013129","DOI":"10.1007\/978-3-319-63046-5_8"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"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\u201375","DOI":"10.1007\/978-3-319-41135-4_4"},{"key":"e_1_2_1_2_18_2","first-page":"188","volume-title":"Lecture Notes in Computer Science","author":"Dybjer Peter","year":"2003"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2430532.2364515"},{"issue":"2","key":"e_1_2_1_2_20_2","first-page":"9","article-title":"Geometric modeling with B: formal specification of generalized maps.","volume":"1","author":"Dubois C","year":"2007","journal-title":"J Sci Pract Comput"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.patcog.2007.02.013"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.02.012"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9117-x"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"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\u201387","DOI":"10.1016\/S0167-5060(08)70696-4"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/978-1-4419-9514-8_6","volume-title":"Random Matrices, Random Processes and Integrable Systems","author":"Eynard B.","year":"2011"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C Paskevich A (2013) Why3\u2014where programs meet provers. In: Proceedings of the 22nd European symposium on programming volume 7792 of LNCS. Springer pp 125\u2013128","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre 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\u2013336","DOI":"10.1007\/978-3-319-40648-0_24"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21215-9_7"},{"key":"e_1_2_1_2_29_2","unstructured":"Gonthier G (2005) A computer checked proof of the Four Colour Theorem. http:\/\/research.microsoft.com\/gonthier\/4colproof.pdf"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Gonthier G (2008) The four colour theorem: engineering of a formal proof. In: ASCM 2007 volume 5081 of LNCS (LNAI). Springer Heidelberg pp 333\u2013333","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_2_1_2_31_2","unstructured":"Giorgetti A Senni V (2012) Specification and validation of algorithms generating planar Lehman words. GASCom\u201912. https:\/\/hal.inria.fr\/hal-00753008"},{"key":"e_1_2_1_2_32_2","unstructured":"Hri\u0163cu C Lampropoulos L D\u00e9n\u00e8s M Paraskevopoulou Z (2018) QuickChick: randomized property-based testing plugin for Coq. https:\/\/github.com\/QuickChick\/QuickChick"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-17333-2","volume-title":"Patterns in permutations and words","author":"Kitaev S","year":"2011"},{"key":"e_1_2_1_2_34_2","unstructured":"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."},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"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\u2013193","DOI":"10.1090\/psapm\/010\/0113289"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Lampropoulos L Gallois-Wong D Hri\u0163cu C Hughes J Pierce BC Xia L (2017) Beginner\u2019s 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\u201320 2017. ACM pp 114\u2013129","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_2_1_2_37_2","unstructured":"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\u20134 2007 volume 8 of Trends in Functional Programming. Intellect pp 105\u2013123"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158133","article-title":"Generating good generators for inductive relations","volume":"2","author":"Lampropoulos Leonidas","year":"2017","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Lando SK Zvonkin AK (2004) Graphs on surfaces and their applications. Springer","DOI":"10.1007\/978-3-540-38361-1"},{"key":"e_1_2_1_2_40_2","unstructured":"Mathematical Components Team (2018) Mathematical components library. http:\/\/math-comp.github.io\/math-comp\/"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10958-017-3555-5"},{"issue":"2","key":"e_1_2_1_2_42_2","first-page":"101","article-title":"A permutations representation that knows what \u201cEulerian\u201d means","volume":"4","author":"Mantaci R","year":"2001","journal-title":"Discrete Math Theor Comput Sci"},{"key":"e_1_2_1_2_43_2","unstructured":"The OEIS Foundation Inc. The on-line encyclopedia of integer sequences. https:\/\/oeis.org\/A000698"},{"key":"e_1_2_1_2_44_2","unstructured":"Owre S (2006) Random testing in PVS. Workshop on Automated Formal Methods (AFM). http:\/\/fm.csl.sri.com\/AFM06\/papers\/5-Owre.pdf"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"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\u201324 2011. ACM pp 91\u201397","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1142\/S021988781550067X"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"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\u201348","DOI":"10.1145\/1543134.1411292"},{"key":"e_1_2_1_2_49_2","unstructured":"Senni V (2018) Validation library. https:\/\/subversion.assembla.com\/svn\/validation\/"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511805967","volume-title":"Enumerative combinatorics, vol 1","author":"Stanley RP","year":"1997"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_1_2_52_2","unstructured":"SWI (2018) Prolog. http:\/\/www.swi-prolog.org\/"},{"key":"e_1_2_1_2_53_2","unstructured":"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\u2013September 4 2015 volume 1433 of CEUR Workshop Proceedings. CEUR-WS.org"},{"key":"e_1_2_1_2_54_2","unstructured":"Tutte WT (1973) What is a map? In: New directions in the theory of graphs: proceedings. Academic Press New York pp 309\u2013325"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1979-091-3"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2011.05.012"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2012.11.030"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(72)90056-1"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0459-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0459-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0459-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0459-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T19:00:45Z","timestamp":1751742045000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0459-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":58,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["10.1007\/s00165-018-0459-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0459-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2018,11]]},"assertion":[{"value":"24 June 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}