Towards platform-independent specification and verification of the standard trigonometry functions

TL;DR

This paper proposes a platform-independent, incremental approach to formally specify and verify standard mathematical functions like sine and cosine, combining manual proofs and computer-assisted validation without relying on specific hardware details.

Contribution

It introduces a novel combined method that integrates manual and computer-aided verification for mathematical functions across different computational platforms.

Findings

Initial specification and verification of cosine and sine functions.

Development of a platform-independent axiomatization of computer arithmetic.

Progress towards a comprehensive verification framework for standard mathematical functions.

Abstract

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.