Skip to Main content Skip to Navigation
Conference papers

Formal study of plane Delaunay triangulation

Abstract : This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay property is achieved. To describe triangulations, we rely on a combinatorial hypermap specification framework we have been developing for years. We embed hypermaps in the plane by attaching coordinates to elements in a consistent way. We then describe what are legal and illegal Delaunay edges and a flipping operation which we show preserves hypermap, triangulation, and embedding invariants. To prove the termination of the algorithm, we use a generic approach expressing that any non-cyclic relation is well-founded when working on a finite set.
Document type :
Conference papers
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Yves Bertot Connect in order to contact the contributor
Submitted on : Monday, July 19, 2010 - 4:09:27 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM
Long-term archiving on: : Friday, October 22, 2010 - 3:53:32 PM


Files produced by the author(s)


  • HAL Id : inria-00504027, version 1
  • ARXIV : 1007.3350




Jean-François Dufourd, Yves Bertot. Formal study of plane Delaunay triangulation. Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.211-226. ⟨inria-00504027⟩



Les métriques sont temporairement indisponibles