Tests and Proofs for Enumerative Combinatorics

  • Catherine Dubois
  • Alain GiorgettiEmail author
  • Richard Genestier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9762)


In this paper we show how the research domain of enumerative combinatorics can benefit from testing and formal verification. We formalize in Coq the combinatorial structures of permutations and maps, and a couple of related operations. Before formally proving soundness theorems about these operations, we first validate them, by using logic programming (Prolog) for bounded exhaustive testing and Coq/QuickChick for random testing. It is an experimental study preparing a more ambitious project about formalization of combinatorial results assisted by verification tools.


Boolean Function Logic Programming Random Testing Exhaustive Testing Enumerative Combinatorics 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



The authors warmly thank the anonymous referees for suggestions, Noam Zeilberger for fruitful discussions and Valerio Senni for advice about his validation library.


  1. 1.
    Berghofer, S., Nipkow, T.: Random testing in Isabelle/HOL. In: Cuellar, J., Liu, Z. (eds.) Software Engineering and Formal Methods (SEFM 2004), pp. 230–239. IEEE Computer Society (2004)Google Scholar
  2. 2.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, New York (2004)CrossRefzbMATHGoogle Scholar
  3. 3.
    Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  4. 4.
    Brun, C., Dufourd, J., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. Comput. Geom. 45(8), 436–457 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bulwahn, L.: The new quickcheck for Isabelle - Random, exhaustive and symbolic testing under one roof. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92–108. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  6. 6.
    Carlier, M., Dubois, C., Gotlieb, A.: Constraint Reasoning in FOCALTEST. In: International Conference on Software and Data Technologies (ICSOFT 2010), Athens, July 2010Google Scholar
  7. 7.
    Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Not., vol. 35, pp. 268–279. ACM, New York (2000)Google Scholar
  8. 8.
    Dubois, C., Mota, J.M.: Geometric modeling with B: formal specification of generalized maps. J. Sci. Pract. Comput. 1(2), 9–24 (2007)Google Scholar
  9. 9.
    Dufourd, J.: Design and formal proof of a new optimal image segmentation program with hypermaps. Pattern Recogn. 40(11), 2974–2993 (2007)CrossRefzbMATHGoogle Scholar
  10. 10.
    Dufourd, J.: Polyhedra genus theorem and Euler formula: a hypermap-formalized intuitionistic proof. Theor. Comput. Sci. 403(2–3), 133–159 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Dufourd, J.: An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps. J. Autom. Reasoning 43(1), 19–51 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 188–203. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Edmonds, J.R.: A combinatorial representation for oriented polyhedral surfaces. Notices Amer. Math. Soc. 7, 646 (1960)Google Scholar
  14. 14.
    Giorgetti, A., Senni, V.: Specification and Validation of Algorithms Generating Planar Lehman Words, June 2012.
  15. 15.
    Gonthier, G.: A computer checked proof of the Four Colour Theorem (2005).
  16. 16.
    Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, pp. 333–333. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Hritcu, C., Lampropoulos, L., Dénès, M., Paraskevopoulou, Z.: Randomized property-based testing plugin for Coq.
  18. 18.
    Kitaev, S.: Patterns in Permutations and Words. Springer, New York (2011)CrossRefzbMATHGoogle Scholar
  19. 19.
    Lando, S.K., Zvonkin, A.K.: Graphs on Surfaces and Their Applications. Springer, New York (2004)CrossRefzbMATHGoogle Scholar
  20. 20.
    Lazarus, F.: Combinatorial graphs and surfaces from the computational and topological viewpoint followed by some notes on the isometric embedding of the square flat torus (2014).
  21. 21.
    Mathematical Components team: Library mathcomp.ssreflect.fingraph.
  22. 22.
    Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM) (2006)Google Scholar
  23. 23.
    Paraskevopoulou, Z., Hritcu, C., Dénès, M., Lampropoulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 325–343. Springer, Heidelberg (2015)Google Scholar
  24. 24.
    Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM/IEEE Conference on Supercomputing, Supercomputing 1991, pp. 4–13. ACM, New York (1991)Google Scholar
  25. 25.
    Runciman, C., Naylor, M., Lindblad, F.: 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 (2008).
  26. 26.
    Seidel, E.L., Vazou, N., Jhala, R.: Type targeted testing. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 812–836. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  27. 27.
    Senni, V.: Validation library.
  28. 28.
  29. 29.
    The OEIS Foundation Inc: The On-Line Encyclopedia of Integer Sequences.
  30. 30.
    Tutte, W.T.: What is a map? In: Harary, F. (ed.) New Directions in the Theory of Graphs: Proceedings, pp. 309–325. Academic Press, New York (1973)Google Scholar
  31. 31.
    Tutte, W.T.: Combinatorial oriented maps. Canad. J. Math. 31(5), 986–1004 (1979)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Catherine Dubois
    • 1
  • Alain Giorgetti
    • 2
    Email author
  • Richard Genestier
    • 2
  1. 1.Samovar (UMR CNRS 5157), ENSIIEÉvryFrance
  2. 2.FEMTO-ST Institute (UMR CNRS 6174 - UBFC/UFC/ENSMM/UTBM), University of Franche-ComtéBesançonFrance

Personalised recommendations