Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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)
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)
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)
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)
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)
Carlier, M., Dubois, C., Gotlieb, A.: Constraint Reasoning in FOCALTEST. In: International Conference on Software and Data Technologies (ICSOFT 2010), Athens, July 2010
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)
Dubois, C., Mota, J.M.: Geometric modeling with B: formal specification of generalized maps. J. Sci. Pract. Comput. 1(2), 9–24 (2007)
Dufourd, J.: Design and formal proof of a new optimal image segmentation program with hypermaps. Pattern Recogn. 40(11), 2974–2993 (2007)
Dufourd, J.: Polyhedra genus theorem and Euler formula: a hypermap-formalized intuitionistic proof. Theor. Comput. Sci. 403(2–3), 133–159 (2008)
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)
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)
Edmonds, J.R.: A combinatorial representation for oriented polyhedral surfaces. Notices Amer. Math. Soc. 7, 646 (1960)
Giorgetti, A., Senni, V.: Specification and Validation of Algorithms Generating Planar Lehman Words, June 2012. https://hal.inria.fr/hal-00753008
Gonthier, G.: A computer checked proof of the Four Colour Theorem (2005). http://research.microsoft.com/gonthier/4colproof.pdf
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)
Hritcu, C., Lampropoulos, L., Dénès, M., Paraskevopoulou, Z.: Randomized property-based testing plugin for Coq. https://github.com/QuickChick
Kitaev, S.: Patterns in Permutations and Words. Springer, New York (2011)
Lando, S.K., Zvonkin, A.K.: Graphs on Surfaces and Their Applications. Springer, New York (2004)
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). http://www.gipsa-lab.grenoble-inp.fr/~francis.lazarus/Documents/hdr-Lazarus.pdf
Mathematical Components team: Library mathcomp.ssreflect.fingraph. http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.fingraph.html
Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM) (2006)
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)
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)
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). http://doi.acm.org/10.1145/1411286.1411292
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)
Senni, V.: Validation library. https://subversion.assembla.com/svn/validation/
SWI: Prolog. http://www.swi-prolog.org/
The OEIS Foundation Inc: The On-Line Encyclopedia of Integer Sequences. https://oeis.org/A000698
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)
Tutte, W.T.: Combinatorial oriented maps. Canad. J. Math. 31(5), 986–1004 (1979)
Acknowledgments
The authors warmly thank the anonymous referees for suggestions, Noam Zeilberger for fruitful discussions and Valerio Senni for advice about his validation library.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Dubois, C., Giorgetti, A., Genestier, R. (2016). Tests and Proofs for Enumerative Combinatorics. In: Aichernig, B., Furia, C. (eds) Tests and Proofs. TAP 2016. Lecture Notes in Computer Science(), vol 9762. Springer, Cham. https://doi.org/10.1007/978-3-319-41135-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-41135-4_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41134-7
Online ISBN: 978-3-319-41135-4
eBook Packages: Computer ScienceComputer Science (R0)