Using PVS to validate the algorithms of an exact arithmetic

摘要

The whole point of exact arithmetic is to generate answers to numeric problems, within some user-specified error. An implementation of exact arithmetic is therefore of questionable value, if it cannot be shown that it is generating correct answers. In this paper, we show that the algorithms used in an exact real arithmetic are correct, A program using the functions defined in this paper has been implemented in 'C' (a HASKELL version of which we provide as an appendix), and we are now convinced of its correctness. The table presented at the end of the paper shows that performing these proofs found three logical errors which had not been discovered by testing. One of these errors was only detected when the theorems were validated with PVS.