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 metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/inria-00504027
Contributor : Yves Bertot <>
Submitted on : Monday, July 19, 2010 - 4:09:27 PM
Last modification on : Wednesday, September 12, 2018 - 1:16:40 AM
Long-term archiving on : Friday, October 22, 2010 - 3:53:32 PM

Files

Del-ITP10.pdf
Files produced by the author(s)

Identifiers

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

Collections

Citation

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⟩

Share

Metrics

Record views

375

Files downloads

374