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.

C. Brun , J-F. Dufourd , N. Magaud

Computational Geometry : Theory and Applications , Volume 45 , Number 8 , page 436--457 - 2012

Additionnal material

International journal
Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq, * Computational Geometry : Theory and Applications*, Elsevier ( IF : 0.476 ), pages 436--457, Volume 45, n° 8, 2012, *doi:10.1016/j.comgeo.2010.06.006*
__Research team__ : IGG

@Article{2-BDM12, author = {Brun, C. and Dufourd, J-F. and Magaud, N.}, title = {Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq}, journal = {Computational Geometry : Theory and Applications}, number = {8}, volume = {45}, pages = {436--457}, year = {2012}, publisher = {ELSEVIER}, doi = {10.1016/j.comgeo.2010.06.006}, x-international-audience = {Yes}, x-language = {EN}, url = {http://icube-publis.unistra.fr/2-BDM12} }

See publications of the same authors