Н. В. Шилов, А. В. Промский
Цена: 50 руб.
Проблема валидации стандартных математических функций и библиотек хорошо осознана профессиональным сообществом, но недостаточно новичками программирования. В статье дано три примера (взятых из педагогического и
исследовательского опыта авторов), демонстрирующих, что формальная спецификация и верификация стандартных функций полезны и даже необходимы.
Ключевые слова: математические функции, стандартные библиотеки, формальная спецификация, формальная верификация.
REFERENCES
1. Harrison, J. Formal verifi cation of square root algorithms. Formal Methods in
System Design, 2003, 22(2), 143–153. doi:10.1023/A:1022973506233
2. Kuliamin, V.V. Standardization and testing of mathematical functions. Lecture
Notes in Computer Science, 2010, 5947, 257–268. doi:10.1007/978-3-642-11486-
1_22
3. Kuliamin, V.V. Standardization and testing of mathematical functions in fl oating point numbers. Programming and Computer Software, 2007, 33(3), 154–173.
doi:10.1134/S036176880703005X
4. Promsky, A. Verifying the standard C library: the C-light approach. Nepomnyaschy, V.A., Sokolov, V.A. (Eds.) Proceeding of the Third Workshop “Program Semantics,
Specifi cation and Verifi cation: Theory and Applications”, 2012, Nizhniy Novgorod,
Russia, pp. 96–103.
5. Promsky, A.V. Experiments on self-applicability in the C-light verifi cation system. Bulletin of Novosibirsk Computing Center, Computer Science Series, 2013, 35,
85–99.
6. Kochan, S.G. Programming in C: A complete introduction to the C programming
language (3rd ed.). 2005, USA: Sam’s Publishing.
7. How to make a program that solves the quadratic formula. Retrieved May 15,
2016, from http://www.youtube.com/watch?v=15NbFrBUdu0
8. Write a C++ program that solves quadratic equation to fi nd its roots. Retrieved
May 15, 2016, from http://www.cplusplus.com/forum/general/36313/
9. C++ refernce. Sqrt, sqrtf, sqrtl. Retrieved May 15, 2016, from http://
en.cppreference.com/w/c/numeric/math/sqrt
10. Gries, D. The science of programming. 1981, USA & Germany: SpringerVerlag.
11. Ayad, A., & Marche, C. Multi-prover verifi cation of fl oating-point programs.
Lecture Notes in Artifi cial Intelligence, 2010, 6173, 127–141. doi:10.1007/978-3-642-
14203-1_11
12. Monniaux, D. The pitfalls of verifying floating-point computations.
ACM Transactions on Programming Languages and Systems, 2008, 30(3), 1–41.
doi:10.1145/1353445.1353446
13. C++ reference. Rand. Retrieved May 15, 2016, from http://en.cppreference.
com/w/c/numeric/random/rand
14. Plauger, P.J. The standard C library. 1992, USA: Prentice Hall.
15. Itsykson, V. The formalism for semantics specifi cation of software libraries.
System Informatics, 2016, 8, 43–52.
