Abstract
The inductive assertion method of Floyd is here applied to programs involving floating point numbers, using a new verification condition generator for C programs known as ProveIt. The exit assertions of such programs need to state that the answers are correct to within some tolerance. We define this notion of tolerance, and show that it is equivalent to Olver's notion of relative precision. As an example, we present an O(ln n) program which takes the nth power of a, and show that the speed of the program does not improve the relative precision, which remains 2n rather than the expected 2 ln n.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Hoare, C. A. R., An axiomatic basis for computer programming, Communications of the ACM 12, 10 (1969), pp. 576–580, 583.
Floyd, R. W., Assigning meanings to programs, Proc. Symp. Applied Math. 19 (Mathematical Aspects of Computer Science), American Mathematical Society, Providence, R. I., 1967, pp. 19–32.
Maurer, W. D., The correctness of computer programs, Part I: preliminary version, Memorandum GWU-IIST-88-23, Institute for Information Science and Technology, George Washington University, August 1988.
Maurer, W. D., Some minimization theorems for verification conditions, 8th International Conference on Computing and Information (ICCI '96), Waterloo, Ontario, Canada, June 1996.
Maurer, W. D., A new method of generating verification conditions, Proc. 1977 Conf. on Information Sciences and Systems, Johns Hopkins Univ., Baltimore, March 1977, pp. 128–133.
Maurer, W. D., The modification index method of generating verification conditions, Proc. 15th Annual Southeast Regional Conf., Biloxi, Miss., April 1977, pp. 426–440.
Ralston, A., and P. Rabinowitz, A First Course In Numerical Analysis (2nd ed.), McGraw-Hill, 1978.
King, J. C., A program verifier, Ph. D. Thesis, Department of Computer Science, Carnegie-Mellon University, 1969.
Subramanian, S., and J. V. Cook, Mechanical verification of C programs, Trusted Information Systems, 444 Castro St., Suite 800, Mountain View, CA.
Olver, F. W. J., A new approach to error arithmetic, SIAM J. Numer. Anal. 15, 2 (Apr. 1978), pp. 368–393.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maurer, W.D. (1997). Relative precision in the inductive assertion method. In: Vulkov, L., Waśniewski, J., Yalamov, P. (eds) Numerical Analysis and Its Applications. WNAA 1996. Lecture Notes in Computer Science, vol 1196. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62598-4_109
Download citation
DOI: https://doi.org/10.1007/3-540-62598-4_109
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62598-8
Online ISBN: 978-3-540-68326-1
eBook Packages: Springer Book Archive