Skip to Main content Skip to Navigation
Journal articles

Designing and proving correct a convex hull algorithm with hypermaps in Coq

Abstract : This article presents the formal design of a functional algorithm which computes the convex hull of a finite set of points incrementally. This algorithm, specified in Coq, is then automatically extracted into an OCaml-program which can be plugged into an interface for data input (point selection) and graphical visualization of the output. A formal proof of total correctness, relying on structural induction, is also carried out. This requires to study many topologic and geometric properties. We use a combinatorial structure, namely hypermaps, to model planar subdivisions of the plane. Formal specifications and proofs are carried out in the Calculus of Inductive Constructions and its implementation: the Coq system.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-00955400
Contributor : Nicolas Magaud <>
Submitted on : Tuesday, March 4, 2014 - 2:25:48 PM
Last modification on : Thursday, January 11, 2018 - 6:22:39 AM
Long-term archiving on: : Wednesday, June 4, 2014 - 11:36:18 AM

File

CGTA2012-BrunDufourdMagaud.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Christophe Brun, Jean-François Dufourd, Nicolas Magaud. Designing and proving correct a convex hull algorithm with hypermaps in Coq. Computational Geometry, Elsevier, 2012, 45 (8), pp.436-457. ⟨10.1016/j.comgeo.2010.06.006⟩. ⟨hal-00955400⟩

Share

Metrics

Record views

427

Files downloads

598