
AbstractWe 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.
interactive theorem proving, combinatorial enumeration, Data structures, random testing, permutations, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-IU]Computer Science [cs]/Ubiquitous Computing, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], logic programming, [INFO.INFO-DC]Computer Science [cs]/Distributed, nteractive theorem proving, rooted maps, bounded-exhaustive testing, Parallel, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, 004, and Cluster Computing [cs.DC], [INFO.INFO-MA]Computer Science [cs]/Multiagent Systems [cs.MA], [INFO.INFO-ET]Computer Science [cs]/Emerging Technologies [cs.ET], Theorem proving (deduction, resolution, etc.)
interactive theorem proving, combinatorial enumeration, Data structures, random testing, permutations, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-IU]Computer Science [cs]/Ubiquitous Computing, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], logic programming, [INFO.INFO-DC]Computer Science [cs]/Distributed, nteractive theorem proving, rooted maps, bounded-exhaustive testing, Parallel, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, 004, and Cluster Computing [cs.DC], [INFO.INFO-MA]Computer Science [cs]/Multiagent Systems [cs.MA], [INFO.INFO-ET]Computer Science [cs]/Emerging Technologies [cs.ET], Theorem proving (deduction, resolution, etc.)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 4 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
