Formal Verification of Mathematical Software. Volume 2

摘要

One of the major problems encountered in trying to formally verify thecorrectness of computer programs that use real arithmetic (hereinafter referred to as mathematical programs) is that the mathematical properties of real arithmetic operations in computers are much more complicated and much harder to work with than the mathematical properties of the corresponding ideal mathematical operations. This occurs because the real number type implemented on a finite computer is not the same as the ideal, mathematical real number type. A finite machine can only represent finitely many different real numbers, whereas there are infinitely many ideal real numbers. The idea behind the theory of asymptotic computing is to develop techniques to prove that the accuracy of a mathematical program goes to infinity (e.g., larger and larger numbers of representation bits for mantissas and exponents used in binary floating point arithmetic). The theory of asymptotic computing, then, is essentially a general formalization of the notions of accuracy and accuracy going to infinity, but without having to show how fast convergence happens (a major source of difficulty in numerical analysis). (kr)