Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня

Цель проекта “Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций” --- инкрементальный комбинированный подход к спецификации и верификации стандартных математических функций, таких как sqrt, cos, sin и так далее. Платформенно-независимый подход предполагает простую аксиоматизацию машинной арифметики в терминах вещественной арифметики (то есть арифметики поля \(\mathbb{R}\) вещественных чисел), не фиксируя ни основание системы счисления, ни формат машинного слова.
Инкрементальность означает, что спецификация и верификация начинается с рассмотрения наиболее “простого” случая – элементарной спецификации и верификации простого алгоритма, работающего с вещественными числами, а заканчивается модификацией элементарной спецификации и алгоритма для машинной арифметики и верификацией алгоритма, работающего в машинной арифметике. А комбинированность подхода означает, что мы начинаем с рассмотрения “базового случая” --- “ручной” верификации (с ручкой и бумагой) для алгоритма, работающего в вещественной арифметике, затем выполняем ручную верификацию алгоритма, работающего в машинной арифметике, используя верификацию для базового случая в качестве “конспекта” (proof-outlines), а заканчиваем --- верификацией с использованием автоматизированной системы построения/поиска доказательства для того, чтобы исключить апелляцию к “очевидности” в ручной верификации. В статье платформенно-независимый инкрементальный комбинированный подход применяется для спецификации и верификации стандартной математической функции квадратного корня. В настоящий момент автоматизированная верификация разработанных алгоритмов выполнена только частично: с использованием системы ACL2 доказана реализуемость (существование) чисел с фиксированной запятой и таблицы начальных приближений квадратного корня.

числа с фиксированной запятой, числа с плавающей запятой, машинная арифметика, формальная верификация, частичная и тотальная корректность, тройки Хоара, метод Флойда, точная функция, квадратный корень, метод Ньютона, справочная таблица

1. Кулямин В.В., “Стандартизация и тестирование реализаций математических функций, работающих с числами с плавающей точкой”, Программирование, 33:3 (2007), 1–29;

2. Никитин В.Ф., Вариант вычисления квадратного корня (алгоритм Ньютона), http://algolist.manual.ru/maths/count_fast/sqrt.php;

3. Шелехов В.И., “Верификация и синтез эффективных программ стандартных функций floor, isqrt и ilog2 в технологии предикатного программирования”, Проблемы управления и моделирования в сложных системах, Труды 12-й межд. конф. (Самара, Самарский научный центр РАН), 2010, 622–630;

4. Ayad A., March ́e 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.

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

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, 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, 102–114, arXiv: 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. Грис Д., Наука программирования, Мир, М., 1986;

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”, Lecture Notes in Computer Science, 1690, Springer, Berlin, Heidelberg, 1999, 113–130.

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

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

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

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

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.

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.

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

21. Muller J.-M., Elementary Functions: Algorithms and Implementation, Birkhau ̈ser, 2005.

22. Muller J.-M. et al., Handbook of Floating-Point Arithmetic, 2nd eddition, Birkhu ̈ser, 2018.

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.

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.

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: 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.

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. Алгоритм нахождения корня n-ной степени, https://ru.wikipedia.org/wiki/%D0% 90%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC_%D0%BD%D0%B0%D1%85%D0%BE%D0% B6%D0%B4%D0%B5%D0%BD%D0%B8%D1%8F_%D0%BA%D0%BE%D1%80%D0%BD%D1%8F_n-%D0%BD% D0%BE%D0%B9_%D1%81%D1%82%D0%B5%D0%BF%D0%B5%D0%BD%D0%B8;

32. “Роскосмос” назвал причину неудачного запуска с космодрома Восточный, https:// www.rbc.ru/politics/12/12/2017/5a2ebcd59a79479d29667115;