Se ha publicado un artículo de razonamiento formalizado en Coq titulado A computer-assisted proof of correctness of a marching cubes algorithm.
Sus autores son Andrey N. Chernikov y Jing Xu (de la Old Dominion University, Norfolk, EEUU).
Su resumen
The Marching Cubes algorithm is a well known and widely used approach for extracting a triangulated isosurface from a three-dimensional rectilinear grid of uniformly sampled data values. The algorithm relies on a large manually constructed table which exhaustively enumerates all possible patterns in which the isosurface can intersect a cubical cell of the grid. For each pattern the table con- tains the local connectivity of the triangles. The construction of this table is labor intensive and error prone. Indeed, the original paper allowed for topological holes in the surface. This problem was later fixed by several authors, however a formal proof of correctness to our knowledge was never presented. In our opinion the most reliable approach to constructing a formal proof for this algorithm is to write a computer program which checks that all the entries in the table satisfy some sufficient condition of correctness. In this paper we present our formal proof which follows this approach, developed with the Coq proof assistant software. The script of our proof can be executed by Coq which verifies that the proof is logically correct, in the sense that its conclusions indeed logically follow from the assumptions. Coq offers a number of helpful features that automate proof development. However, Coq cannot check that the development corresponds to the problem we wish to solve, therefore, this correspondence is elaborated upon in this paper. Our complete Coq development is available online.
El trabajo se presentará en octubre en el 22nd International Meshing Roundtable.