Abstract : This article presents a generic method to build programs in computational geometry from their specifications. It focuses on a case study namely computing incrementally the convex hull of a set of points in the plane. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification.
https://hal.inria.fr/hal-00916880
Contributeur : Nicolas Magaud
<>
Soumis le : mardi 10 décembre 2013 - 20:13:20
Dernière modification le : samedi 13 janvier 2018 - 01:02:58
Document(s) archivé(s) le : mardi 11 mars 2014 - 16:30:11
