Preuves formelles pour le calcul d'enveloppes convexes dans le plan avec des hypercartes
Institution:
StrasbourgDisciplines:
Directors:
Abstract EN:
Our aim is to lead a formal survey in geometric modeling and computational geometry in order to improve the programming techniques and ensure the algorithms correctness. The originality of the means we use to achieve our purpose rely on one hand on the fact that the specifications and the formai proofs of programs are expressed in the formalism of the Calculus of Inductive Constructions implemented in the Coq system, and on the other hand on the fact that we work in a topology-based geometric modeling framework where the planar subdivisions are described by combinatorial oriented maps. We present a formai case study in computational geometry on a classical problem which involves elementary geometric objects: computing the incremental convex hull ofa finite collection ofplanar points. Our work consists in designing two functional convex hull algorithms, automatically extracting a program in OCaml augmented with input handling and a graphical display of the result, and formally proving their total correctness. Proofs consist in checking the termination of the algorithms as well as highlighting several useful topologic and geometric properties. Finally, we derive a C++ implementation of an optimized program from our specification and integrate it into the library developped in our team.
Abstract FR:
Notre objectif est de mener une étude formelle dans le domaine de la modélisation géométrique et de la géométrie algorithmique dans le plan afin d'améliorer les techniques de programmation et d'assurer la correction des algorithmes. Nous nous appuyons, d'une part sur les méthodes de spécifications et de preuves formelles du système d'aide à la preuve Coq, et d'autre part sur un cadre de modélisation géométrique à base topologique où les subdivisions du plan sont représentées par des hypercartes. Nous avons mené une étude de cas en géométrie algorithmique sur un problème classique mettant enjeu des subdivisions de surfaces simples puisque réduites à des lignes polygonales : le calcul incrémentaI de l'enveloppe convexe d'un ensemble fmi de points du plan. Nous avons conçu deux algorithmes fonctionnels en Coq dont nous avons extrait automatiquement un programme en OCaml. Puis, nous avons démontré formellement leur correction par la mise en évidence de leurs propriétés topologiques et géométriques. Finalement, nous avons procédé à la dérivation d'un programme efficace en langage impératif (C+) pour une insertion dans la plate-forme de modélisation géométrique de notre équipe.