Verifiable implementations of geometric algorithms using finite precision arithmetic (Q1116270)

The author discusses two methods for handling round-off errors in finite precision implementations of geometric algorithms. The first method, called data normalization, replaces a given geometric structure by another structure, approximating the original one, and belonging to a set of legal inputs. This set of inputs is defined by restricting the set of accepted configurations to those satisfying certain metric and topological constraints. The method is applied to the modeling of planar polygon regions, where the results of the various geometric operations are corrected by a basic operation of ``accomodation'' which, in turn, uses two primitive operations of ``vertex shifting'' and ``edge cracking''. The second method, called the hidden variable method, replaces the original structure by a simplified structure with parameters in an infinite precision domain. The method is applied to the problem of determining the topological arrangement of lines in the plane. The new structure replaces a bundle of lines sitting close to each other by a curve satisfying a property of ``approximate monotonicity'' and approximating a straight line; the number of intersection points and their order relations are kept unchanged. Both methods are shown to provide provably correct finite precision implementations on their legal inputs. The author discusses the various advantages and disadvantages of his two methods; he also provides pseudocode descriptions of their algorithmic implementations.