Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls.

This article deals with a 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 using hypermaps. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. It performs a recursive traversal of the existing convex hull to compute the new hull each time a new point is inserted. This requires using well-founded recursion in Coq. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification.