Skip to main content
SpringerLink
Log in

Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls

  • Conference paper
Automated Deduction in Geometry (ADG 2012)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 7993))

Included in the following conference series:

  • 537 Accesses

Abstract

This article deals with a method to build programs in computational geometry from their specifications. It focuses on a case study namely computing incrementally the convex hull of a set of points in the plane using hypermaps. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. It performs a recursive traversal of the existing convex hull to compute the new hull each time a new point is inserted. This requires using well-founded recursion in Coq. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification.

This work was supported by the french ANR project Galapagos (2008-2011).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C.: Verification of Certifying Computations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 67–82. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  2. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, An EATCS Series. Springer (2004)

    Google Scholar 

  3. Bertot, Y., Magaud, N., Zimmermann, P.: A Proof of GMP Square Root. Journal of Automated Reasoning 29(3-4), 225–252 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bertrand, Y., Dufourd, J.-F., Françon, J., Lienhardt, P.: Algebraic Specification and Development in Geometric Modeling. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 75–89. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  5. Brun, C., Dufourd, J.-F., Magaud, N.: Formal Proof of the Incremental Convex Hull Algorithm, http://galapagos.gforge.inria.fr

  6. Brun, C., Dufourd, J.-F., Magaud, N.: Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq. Computational Geometry, Theory and Applications 45(8), 436–457 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  7. CEA-INRIA. The Frama-C Software Verification Toolkit, http://frama-c.cea.fr

  8. Coq Development Team. The Coq Proof Assistant - Reference Manual and Library, http://coq.inria.fr/

  9. Cori, R.: Un code pour les graphes planaires et ses applications. Astérisque, vol. 27. Socieété mathématique de France (1970)

    Google Scholar 

  10. de Berg, M., Cheong, O., van Kreveld, M., Overmars, M.: Computational Geometry, Algorithms and Applications. Springer (2008)

    Google Scholar 

  11. Dufourd, J.-F.: Design and Formal Proof of a New Optimal Image Segmentation Program with Hypermaps. Pattern Recognition 40(11), 2974–2993 (2007)

    Article  MATH  Google Scholar 

  12. Dufourd, J.-F.: An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps. Journal of Automated Reasoning 43(1), 19–51 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  13. Dufourd, J.-F., Bertot, Y.: Formal Study of Plane Delaunay Triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 211–226. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Edelsbrunner, H.: Algorithms in Combinatorial Geometry. Monographs in Theoretical Computer Science, An EATCS Series. Springer (1987)

    Google Scholar 

  15. Flato, E., Halperin, D., Hanniel, I., Nechushtan, O.: The Design and Implementation of Planar Maps in CGAL. In: Vitter, J.S., Zaroliagis, C.D. (eds.) WAE 1999. LNCS, vol. 1668, pp. 154–168. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Gonthier, G.: Formal Proof - The Four-Colour Theorem. Notices of the AMS 55(11), 1382–1393 (2008)

    MathSciNet  MATH  Google Scholar 

  17. IGG Team. CGoGN: Combinatorial and Geometric mOdeling with Generic N-dimensional Maps, https://iggservis.u-strasbg.fr/CGoGN/

  18. Kettner, L., Mehlhorn, K., Pion, S., Schirra, S., Yap, C.-K.: Classroom Examples of Robustness Problems in Geometric Computations. Computational Geometry 40(1), 61–78 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  19. Knuth, D.E.: Axioms and Hulls. LNCS, vol. 606. Springer, Heidelberg (1992)

    Book  MATH  Google Scholar 

  20. Lienhardt, P.: Topological Models for Boundary Representation: a Comparison with n-Dimensional Generalized Maps. Computer-Aided Design 23, 59–82 (1991)

    MATH  Google Scholar 

  21. Meikle, L.I., Fleuriot, J.D.: Mechanical Theorem Proving in Computational Geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol. 3763, pp. 1–18. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame graphs. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 21–35. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Pichardie, D., Bertot, Y.: Formalizing Convex Hull Algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 346–361. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ICube, UMR 7357, University of Strasbourg - CNRS, 300 bd Sébastien Brant, BP 10413, 67412, Illkirch Cedex, France

    Christophe Brun, Jean-François Dufourd & Nicolas Magaud

Authors
  1. Christophe Brun
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-François Dufourd
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nicolas Magaud
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, 1006, Laboratory of Advanced Research, University of Tsukuba, 305-8573, Tsukuba, Japan

    Tetsuo Ida

  2. School of Informatics, Informatics Forum, University of Edinburgh, 10 Crichton Street, EH8 9AB, Edinburgh, UK

    Jacques Fleuriot

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brun, C., Dufourd, JF., Magaud, N. (2013). Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. In: Ida, T., Fleuriot, J. (eds) Automated Deduction in Geometry. ADG 2012. Lecture Notes in Computer Science(), vol 7993. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40672-0_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40672-0_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40671-3

  • Online ISBN: 978-3-642-40672-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation