Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня
Аннотация
Инкрементальность означает, что спецификация и верификация начинается с рассмотрения наиболее “простого” случая – элементарной спецификации и верификации простого алгоритма, работающего с вещественными числами, а заканчивается модификацией элементарной спецификации и алгоритма для машинной арифметики и верификацией алгоритма, работающего в машинной арифметике. А комбинированность подхода означает, что мы начинаем с рассмотрения “базового случая” --- “ручной” верификации (с ручкой и бумагой) для алгоритма, работающего в вещественной арифметике, затем выполняем ручную верификацию алгоритма, работающего в машинной арифметике, используя верификацию для базового случая в качестве “конспекта” (proof-outlines), а заканчиваем --- верификацией с использованием автоматизированной системы построения/поиска доказательства для того, чтобы исключить апелляцию к “очевидности” в ручной верификации. В статье платформенно-независимый инкрементальный комбинированный подход применяется для спецификации и верификации стандартной математической функции квадратного корня. В настоящий момент автоматизированная верификация разработанных алгоритмов выполнена только частично: с использованием системы ACL2 доказана реализуемость (существование) чисел с фиксированной запятой и таблицы начальных приближений квадратного корня.
Об авторах
Николай Вячеславович ШиловРоссия
канд. физ.-мат. наук, доцент
ул. Университетская, 1, г. Иннополис, Республика Татарстан, 420500
Дмитрий Александрович Кондратьев
Россия
аспирант
пр. акад. Лаврентьева, 6, г. Новосибирск, 630090
Игорь Сергеевич Ануреев
Россия
канд. физ.-мат. наук, ст. науч. сотр.
пр. акад. Лаврентьева, 6, г. Новосибирск, 630090
Евгений Викторович Бодин
Россия
науч. сотр.
пр. акад. Лаврентьева, 6, г. Новосибирск, 630090
Алексей Владимирович Промский
Россия
канд. физ.-мат. наук, ученый секретарь
пр. акад. Лаврентьева, 6, г. Новосибирск, 630090
Список литературы
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;
Для цитирования:
Шилов Н.В., Кондратьев Д.А., Ануреев И.С., Бодин Е.В., Промский А.В. Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня. Моделирование и анализ информационных систем. 2018;25(6):637-666. https://doi.org/10.18255/1818-1015-2018-6-637-666
For citation:
Shilov N.V., Kondratyev D.A., Anureev I.S., Bodin E.V., Promsky A.V. Platform-independent Specification and Verification of the Standard Mathematical Square Root Function. Modeling and Analysis of Information Systems. 2018;25(6):637-666. (In Russ.) https://doi.org/10.18255/1818-1015-2018-6-637-666