Platform-Independent Specification and Verification of the Standard Mathematical Square Root Function | Automatic Control and Computer Sciences Skip to main content
Springer Nature Link
Log in

Platform-Independent Specification and Verification of the Standard Mathematical Square Root Function

  • Published:
Automatic Control and Computer Sciences Aims and scope Submit manuscript

Abstract

The aim of the Platform-Independent Approach to Formal Specification and Verification of Standard Mathematical Functions project is the development of an incremental combined approach to specification and verification of standard mathematical functions like sqrt, cos, sin, etc. The term “platform-independence” means that we attempt to design a relatively simple axiomatization of computer arithmetic in terms of real arithmetic (i.e., the arithmetic of the field ℝ of real numbers), but do not specify either the base of the computer arithmetic or the format of the representation of numbers. The incrementality means that we start with the most straightforward specification of the simplest algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetic. We call our approach combined because we start with consideration of a “basic” case, the manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for the manual verification of the algorithm in computer arithmetic, 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. By now, the computer-aided validation of the developed algorithms has been carried out only partially to prove, using the ACL2 system, the correctness (consistency) of our fixed-point arithmetic and the existence of a look-up table with the initial approximations of the square roots for fixed-point numbers.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1.
Fig. 2.
Fig. 3.
Fig. 4.
Fig. 5.
Fig. 6.
Fig. 7.

Similar content being viewed by others

Notes

  1. Here and below, \(\lambda \,\,z \in \mathbb{R}.\left\lceil z \right\rceil \) is the rounding up to the nearest integer.

REFERENCES

  1. Kuliamin, V.V., Standardization and testing of implementations of mathematical functions in floating point numbers, Program. Comput. Software, 2007, vol. 33, no. 3, pp. 154–173.

    Article  MathSciNet  Google Scholar 

  2. Nikitin, V.F., A variant for calculating the square root (Newton’s algorithm). http://algolist.manual.ru/ maths/count_fast/sqrt.php.

  3. Shelekhov, V.I., Verification and synthesis of effective programs of standard functions floor, isqrt, and ilog2 in predicate programming technology, Problemy upravleniya i modelirovaniya v slozhnykh sistemakh, Trudy 12-i mezhd. konf. (Problems of Control and Modeling in Complex Systems, Proc. 12th Int. Conf.), Samara, 2010, pp. 622–630.

  4. Ayad, A. and Marché, C., Multi-prover verification of floating-point programs, Perspectives of System Informatics. PSI 2014; Lect. Notes Artif. Intell., 2010, vol. 6173, pp. 127–141.

    MATH  Google Scholar 

  5. Barret, G., Formal methods applied to a floating-point number system, IEEE Trans. Software Eng., 1989, vol. 15, no. 5, pp. 611–621.

    Article  Google Scholar 

  6. Brain, M., et al., An automatable formal semantics for IEEE-754 floating-point arithmetic, Computer Arithmetic (ARITH ‘15), Proc. of the 2015 IEEE 22nd Symposium (IEEE Computer Society), 2015, pp. 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), arXiv: arXiv:1708.00140, 2017, pp. 102–114.

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

    Google Scholar 

  10. Gries, D., The Science of Programming, New York: Springer-Verlag, 1981.

    Book  Google Scholar 

  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: arXiv:physics/0302034.

  13. Harrison, J., A machine-checked theory of floating point arithmetic, Lect. Notes Comput. Sci., 1999, vol. 1690, pp. 113–130.

    Article  Google Scholar 

  14. Harrison, J., Formal verification of floating point trigonometric functions, Lect. Notes Comput. Sci., 2000, vol. 1954, pp. 217–251.

    Article  Google Scholar 

  15. Harrison, J., Formal verification of IA-64 division algorithms, Lect. Notes Comput. Sci., 2000, vol. 1869, pp. 233–251.

    Article  Google Scholar 

  16. Harrison, J., Floating point verification in HOL light: The exponential function, Formal Methods Syst. Des., 2000, vol. 16, no. 3, pp. 271–305.

    Article  Google Scholar 

  17. Harrison, J., Formal verification of square root algorithms, Formal Methods Syst. Des., 2003, vol. 22, no. 2, pp. 143–153.

    Article  Google Scholar 

  18. Hoare, C.A.R., The verifying compiler: A grand challenge for computing research, Lect. Notes Comput. Sci., 2003, vol. 2890, pp. 1–12.

    MATH  Google Scholar 

  19. Kuliamin, V.V., Standardization and testing of mathematical functions in floating point numbers, Lect. Notes Comput. Sci., 2010, vol. 5947, pp. 257–268.

    Article  Google Scholar 

  20. Monniaux, D., The pitfalls of verifying floating-point computations, ACM Trans. Program. Languages Syst., 2008, vol. 30, no. 3, pp. 1–41.

    Article  Google Scholar 

  21. Muller, J.-M., Elementary Functions: Algorithms and Implementation, Birkhäuser, 2005.

    Google Scholar 

  22. Muller, J.-M., et al., Handbook of Floating-Point Arithmetic, Birkhäuser, 2018, 2nd ed.

    Book  Google Scholar 

  23. Sawada, J. and Gamboa, R., Mechanical verification of a square root algorithm using Taylor’s theorem, Lect. Notes Comput. Sci., 2002, vol. 2517, pp. 274–291.

    Article  Google Scholar 

  24. Shilov, N.V., On the need to specify and verify standard functions, Bull. Novosib. Comput. Center (Ser.: Comput. Sci.), 2015, vol. 38, pp. 105–119.

  25. Shilov, N.V. and Promsky, A.V., On specification and verification of standard mathematical functions, Humanit. Sci. Univ. J., 2016, vol. 19, pp. 57–68.

    Google Scholar 

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

  27. Siddique, U. and Hasan, O., On the formalization of gamma function in HOL, J. Autom. Reason., 2014, vol. 53, no. 4, pp. 407–429.

    Article  MathSciNet  Google Scholar 

  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 named reason for failured launch from space center Vostochny. https://www.rbc.ru/politics/ 12/12/2017/5a2ebcd59a79479d29667115.

Download references

ACKNOWLEDGMENTS

The authors are grateful to D.Yu. Nadezhin for the very helpful consultations on ACL2 proof-assistant system and participation in discussing the content of preprint [26].

Funding

This work was supported by the Russian Foundation for Basic Research, project no. 17-01-00789.

Author information

Authors and Affiliations

  1. Autonomous Noncommercial Organization of Higher Education “Innopolis University”, 420500, Innopolis, Republic of Tatarstan, Russia

    N. V. Shilov

  2. Ershov Institute of Informatics Systems, Siberian Branch, Russian Academy of Sciences, 630090, Novosibirsk, Russia

    D. A. Kondratyev, I. S. Anureev, E. V. Bodin & A. V. Promsky

  3. Institute of Automation and Electrometry, 630060, Novosibirsk, Russia

    I. S. Anureev

Authors
  1. N. V. Shilov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. D. A. Kondratyev
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. I. S. Anureev
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. E. V. Bodin
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. A. V. Promsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to N. V. Shilov, D. A. Kondratyev, I. S. Anureev, E. V. Bodin or A. V. Promsky.

Ethics declarations

The authors declare that they have no conflicts of interest.

Additional information

Translated by O. Lotova

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Shilov, N.V., Kondratyev, D.A., Anureev, I.S. et al. Platform-Independent Specification and Verification of the Standard Mathematical Square Root Function. Aut. Control Comp. Sci. 53, 595–616 (2019). https://doi.org/10.3103/S0146411619070186

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.3103/S0146411619070186

Keywords:

Search

Navigation