2019/01/10 by Н. В. Шилов, Shilov, Nikolay V., Boris L. Faifel +5
Computer Science · #F.3.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Numerical Methods and Algorithms
paper · pdf · doi:10.48550/arxiv.1901.03414
openalex publication_date 2019/01/10 · openalex created_date 2019/01/25 · openalex updated_date 2026/07/28
Research project "Platform-independent approach to formal specification and verification of standard mathematical functions" is aimed onto a development of an incremental combined approach to the specification and verification of the standard mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetic in terms of real, rational, and integer arithmetic (i.e. the fields R and Q of real and rational numbers, the ring Z of integers) but don't specify neither base of the computer arithmetic, nor a format of numbers' representation. Incrementality means that we start with the most straightforward specification of the simplest easy to verify algorithm in real numbers and finish with a realistic specification and a verification of an algorithm in computer arithmetic. We call our approach combined because we start with a manual (pen-and-paper) verification of some selected algorithm in real numbers, then use these algorithm and verification as a draft and proof-outlines for the algorithm in computer arithmetic and its manual verification, and finish with a computer-aided validation of our manual proofs with some proof-assistant system (to avoid appeals to "obviousness" that are very common in human-carried proofs). In the paper we present first steps towards a platform-independent incremental combined approach to specification and verification of the standard functions cos and sin that implement mathematical trigonometric functions cos and sin.