N. V. Shilov, A. V. Promsky
Price: 50 руб.
The problem of validating standard mathematical functions and libraries is well-recognized by industrial and academic professional community, but still is poorly understood by freshmen and inexperienced developers. The paper gives three examples (from authors’ pedagogical and research experience) when formal specifi cation and verifi cation of standard functions are useful and essential.
Keywords: mathematical functions, standard libraries, formal specifi cation, formal program verifi cation.
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.
