Abstract
This paper outlines the PVS development for the inverse trigonometric functions: atan(x), asin(x) and acos(x). This is then used to validate exact arithmetic algorithms based on fast binary cauchy sequences [14, 17] for these functions in a further PVS development.
The principle results of using PVS in this process is the detection of four errors in an implementation that had previously been believed to be correct. In addition, an error was detected in the handbook of formulæ used (Abramowitz and Stegun, Formula 4.4.34).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramovitz, M., Stegun, I.A.: Handbook of Mathematical Functions, 9th edn. Dover Publications, New York (1972)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–580 (1969)
Ko, K.-I.: On the definitions of some complexity classes of real numbers. Math. Systems Theory 16, 95–109 (1983)
Lee Jr., V.A., Boehm, H.-J.: Optimizing programs over the constructive reals. In: Proceedings of the ACM SIGPLAN 1990 conference on Programming Language design and implementation, pp. 102–111 (1990)
Lester, D.R., Gowland, P.: Using PVS to validate the algorithms of an exact arithmetic. In: TCS, vol. 291, pp. 203–218 (2003)
Ménissier-Morain, V.: Arithmétique exacte, Ph.D. thesis, L’Université Paris VII (December 1994)
Mostowski, A.: On computable sequences. Fundamenta Mathematicae 44, 37–51 (1957)
Müller, N.T.: Subpolynomial complexity classes of real functions and real numbers. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 284–293. Springer, Heidelberg (1986)
Müller, N.T.: Towards a real Real RAM: a prototype using C++. In: Ko, K.-I., Müller, N., Weihrauch, K. (eds.) Computability and Complexity in Analysis. second CCA Workshop, August 22-23, pp. 59–66. Universität Trier, Trier (1996)
Müller, N.T.: Implementing limits in an interactive RealRAM. In: Chesneaux, J.-M., Jézéquel, F., Lamotte, J.-L., Vignes, J. (eds.) Third Real Numbers and Computers Conference, paris, France, April 27-29, pp. 59–66. Université Pierre et Marie Curie, Paris (1998)
Owre, S., Shaker, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide, Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999), Available from http://pvs.csl.sri.com
Pour-El, M.B., Richards, J.I.: Computability in Analysis and Physics. In: Perspectives in Mathematical Logic, Springer, Berlin (1989)
Rice, H.: Recursive real numbers. Proc. Amer. Math. Soc. 5, 784–791 (1954)
Robinson, R.: Review of “Peter, R., Rekursive Funktionen”. The Journal of Symbolic Logic 16, 280–282 (1951)
Specker, E.: Nicht konstruktiv beweisbare Sätze der Analysis. The Journal of Symbolic Logic 14(3), 145–158 (1949)
Weihrauch, K.: Computability. EATCS Monographs on Theoretical Computer Science, vol. 9. Springer, Berlin (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lester, D. (2004). Using PVS to Validate the Inverse Trigonometric Functions of an Exact Arithmetic. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds) Numerical Software with Result Verification. Lecture Notes in Computer Science, vol 2991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24738-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-24738-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21260-7
Online ISBN: 978-3-540-24738-8
eBook Packages: Springer Book Archive