Formal study of plane Delaunay triangulation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Formal study of plane Delaunay triangulation

Résumé

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.
Cet article présente la preuve formelle de correction d'un algorithme de triangulation de Delaunay. L'algorithme consiste à répéter une opération de basculement d'arête à partir d'une triangulation initial jusqu'à ce que la propriété de Delaunay soit satisfaite. Pour décrire les triangulations, nous utilisons un cadre formel d'hypercartes combinatoires que nous développons depuis des années. Nous plongeons les hypercartes dans le plan en attachant des coordonnées aux élément de l'hypercarte de façon cohérente. Nous décrivons ensuite quelles sont les arêtes illégales pour Delaunay et comment fonctionne l'opération de basculement, pour laquelle nous montrons la préservations des structures d'hypercarte, de triangultion, et de plongement. Pour prouver la terminaison de l'algorithme, nous utilisons une approche générique exprimant que toute relation non-cyclic sur un ensemble fini est bien fondée.
Fichier principal
Vignette du fichier
Del-ITP10.pdf (180.78 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00504027 , version 1 (19-07-2010)

Identifiants

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

Citer

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⟩
233 Consultations
284 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More