1. Tests and proofs for custom data generators
- Author
-
Alain Giorgetti, Catherine Dubois, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), and Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)
- Subjects
combinatorial enumeration ,Theoretical computer science ,random testing ,Computer science ,media_common.quotation_subject ,permutations ,0102 computer and information sciences ,02 engineering and technology ,[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] ,Mathematical proof ,01 natural sciences ,Theoretical Computer Science ,[INFO.INFO-IU]Computer Science [cs]/Ubiquitous Computing ,logic programming ,[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] ,0202 electrical engineering, electronic engineering, information engineering ,Logic programming ,media_common ,nteractive theorem proving ,Proof assistant ,rooted maps ,Random testing ,020207 software engineering ,bounded-exhaustive testing ,[INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation ,Enumerative combinatorics ,Debugging ,010201 computation theory & mathematics ,[INFO.INFO-MA]Computer Science [cs]/Multiagent Systems [cs.MA] ,Bounded function ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,[INFO.INFO-ET]Computer Science [cs]/Emerging Technologies [cs.ET] ,[INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC] ,Software ,Counterexample - Abstract
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.
- Published
- 2018