Platform-independent specification and verification of the standard mathematical square root function

N. V. Shilov ; D. A. Kondratyev ; I. S. Anureev ; E. V. Bodin ; A. V. Promsky

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 637-666.

Résumé

The project “Platform-independent approach to formal specification and verification of standard mathematical functions” is aimed onto the development of incremental combined approach to specification and verification of standard Mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetics in terms of real arithmetics (i.e. the field $\mathbb{R}$ of real numbers) but do not specify neither base of the computer arithmetics, nor a format of numbers representation. Incrementality means that we start with the most straightforward specification of the simplest case to verify the algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetics. We call our approach combined because we start with manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for a manual verification of the algorithm in computer arithmetics, and finish with a computer-aided validation of the manual proofs with a proof-assistant system (to avoid appeals to “obviousness” that are common in human-carried proofs). In the paper, we apply our platform-independent incremental combined approach to specification and verification of the standard Mathematical square root function. Currently a computer-aided validation was carried for correctness (consistency) of our fix-point arithmetics and for the existence of a look-up table with the initial approximations of the square roots for fix-point numbers.

Détail

Keywords: fix-point numbers, floating-point numbers, computer arithmetic, formal verification, partial and total correctness, Hoare triples, Floyd verification method of inductive assertions, exact function, square root function, Newton–Raphson method, look-up table.

Bibliographie

[1] Kuliamin V.V., “Standardization and testing of implementations of mathematical functions in floating point numbers”, Programming and Computer Software, 33:3 (2007), 154–173 | DOI | MR | Zbl

[2] Nikitin V.F., Variant vychisleniya kvadratnogo kornya (algoritm Nyutona) (in Russian)

[3] Shelekhov V.I., “Verifikatsiya i sintez effektivnykh programm standartnykh funktsiy floor, isqrt i ilog2 v tekhnologii predikatnogo programmirovaniya”, Problemy upravleniya i modelirovaniya v slozhnykh sistemakh, Trudy 12-y mezhd. konf. (Samara, Samarskiy nauchnyy tsentr RAN, 2010), 622–630 (in Russian)

[4] Ayad A., Marché C., “Multi-prover verification of floating-point programs”, Perspectives of System Informatics, PSI 2014, Lecture Notes in Artificial Intelligence, 6173, Springer, Berlin–Heidelberg, 2010, 127–141 | Zbl

[5] Barret G., “Formal Methods Applied to a Floating-Point Number System”, IEEE Trans. Softw. Eng., 15:5 (1989), 611–621 | DOI

[6] Brain M. et al., “An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic”, Computer Arithmetic, Proc. of the 2015 IEEE 22nd Symposium ARITH '15, IEEE Computer Society, 2015, 160–167

[7] El-Magdoub M.H., Best Square Root Method – Algorithm – Function (Precision VS Speed), https://www.codeproject.com/Articles/69941/Best-Square-Root-Method-Algorithm-Function-Precisi

[8] Ferguson W.E. et al., Digit serial methods with applications to division and square root (with mechanically checked correctness proofs), 2017, arXiv: 1708.00140

[9] Gamboa R.A., Square Roots in Acl2: a Study in Sonata Form, Technical Report, University of Texas at Austin, USA, 1997

[10] Gries D., The Science of Programming, Springer-Verlag, New York, 1981 | MR | Zbl

[11] Grohoski G., “Verifying Oracle's SPARC Processors with ACL2”, Slides of the Invited talk, The ACL2 Theorem Prover and Its Applications, Proc. Int. Workshop, 2017 http://www.cs.utexas.edu/users/moore/acl2/workshop-2017/slides-accepted/grohoski-ACL2_talk.pdf

[12] Gutowski M.W., Power and beauty of interval methods, arXiv: physics/0302034

[13] Harrison J., “A Machine-Checked Theory of Floating Point Arithmetic”, Lecture Notes in Computer Science, 1690, Springer, Berlin–Heidelberg, 1999, 113–130 | DOI

[14] Harrison J., “Formal Verification of Floating Point Trigonometric Functions”, Lecture Notes in Computer Science, 1954, Springer, Berlin–Heidelberg, 2000, 217–233 | DOI

[15] Harrison J., “Formal Verification of IA-64 Division Algorithms”, Lecture Notes in Computer Science, 1869, Springer, Berlin–Heidelberg, 2000, 233–251 | DOI | Zbl

[16] Harrison J., “Floating Point Verification in HOL Light: The Exponential Function”, Formal Methods in System Design, 16:3 (2000), 271–305 | DOI

[17] Harrison J., “Formal Verification of Square Root Algorithms”, Formal Methods in System Design, 22:2 (2003), 143–153 | DOI | Zbl

[18] Hoare C.A.R., “The Verifying Compiler: A Grand Challenge for Computing Research”, Lecture Notes in Computer Science, 2890, Springer, Berlin–Heidelberg, 2003, 1–12 | MR

[19] Kuliamin V.V., “Standardization and Testing of Mathematical Functions in floating point numbers”, Lecture Notes in Computer Science, 5947, Springer, Berlin–Heidelberg, 2010, 257–268 | DOI | Zbl

[20] Monniaux D., “The pitfalls of verifying floating-point computations”, ACM Transactions on Programming Languages and Systems, 30:3 (2008), 1–41 | DOI

[21] Muller J.-M., Elementary Functions: Algorithms and Implementation, Birkhaüser, 2005 | MR

[22] Muller J.-M. et al., “Verifying Floating-Point Algorithms”, Handbook of Floating-Point Arithmetic, 2nd edition, Birkhüser, 2018, 479–511 | DOI

[23] Sawada J., Gamboa R., “Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem”, Lecture Notes in Computer Science, 2517, Springer, Berlin–Heidelberg, 2002, 274–291 | DOI | Zbl

[24] Shilov N.V., “On the need to specify and verify standard functions”, The Bulletin of the Novosibirsk Computing Center (Series: Computer Science), 38 (2015), 105–119 | Zbl

[25] Shilov N.V., Promsky A.V., “On specification andd verification of standard mathematical functions”, Humanities and Science University Journal, 19 (2016), 57–68

[26] Shilov N.V. et al., Towards platform-independent verification of the standard mathematical functions: the square root function, arXiv: abs/1801.00969

[27] Siddique U., Hasan O., “On the Formalization of Gamma Function in HOL”, J. Autom. Reason., 53:4 (2014), 407–429 | DOI | MR | Zbl

[28] C reference. Sqrt, sqrtf, sqrtl, http://en.cppreference.com/w/c/numeric/math/sqrt

[29] IEEE 754-2008, http://ieeexplore.ieee.org/document/4610935

[30] ISO/IEC/IEEE 60559:2011. Information technology – Microprocessor Systems – Floating-Point arithmetic, http://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumber=57469

[31] nth root algorithm, https://en.wikipedia.org/wiki/Nth_root_algorithm

[32] “Roskosmos” nazval prichinu neudachnogo zapuska s kosmodroma Vostochnyy (in Russian)