LoginRegistration
For instance: The Scientific Opinion
About consortium subscription Contacts
(812) 923 41 97 Non-commercial partnership
St. Petersburg
university
consortium
Your order
0
To the amount of:
0
руб.
Empty
View

Статьи

"The Scientific Opinion" №12 (Psycho-pedagogical and philosophy of science), 2016

On Specifi cation and Verifi cation of Standard Mathematical Functions

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.
Price: 50 рублей
To order