Designing and proving correct a convex hull algorithm with hypermaps in Coq

详细信息	查看全文 | 推荐本文 |

• 作者：Christophe Brun ^{brun@lsiit-cnrs.unistra.fr} ; Jean-Franç ; ois Dufourd ^{dufourd@lsiit-cnrs.unistra.fr} ; Nicolas Magaud ; ^{magaud@lsiit-cnrs.unistra.fr}
• 关键词：Convex hull ; Hypermaps ; Formal specifications ; Computer-aided proofs ; Coq system
• 刊名：Computational Geometry
• 出版年：2012
• 期刊代码：18_09257721
• 类别：cp
• 出版时间：October, 2012
• 卷：45
• 期：8
• 页码：436-457
• 文件大小：552 K

摘要

This article presents the formal design of a functional algorithm which computes the convex hull of a finite set of points incrementally. This algorithm, specified in Coq, is then automatically extracted into an OCaml program which can be plugged into an interface for data input (point selection) and graphical visualization of the output. A formal proof of total correctness, relying on structural induction, is also carried out. This requires to study many topologic and geometric properties. We use a combinatorial structure, namely hypermaps, to model planar subdivisions of the plane. Formal specifications and proofs are carried out in the Calculus of Inductive Constructions and its implementation: the Coq system.