Platform-independent specification and verification of the standard mathematical square root function

N. V. Shilov ; D. A. Kondratyev ; I. S. Anureev ; E. V. Bodin ; A. V. Promsky

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 637-666

Résumé

The project “Platform-independent approach to formal specification and verification of standard mathematical functions” is aimed onto the development of incremental combined approach to specification and verification of standard Mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetics in terms of real arithmetics (i.e. the field $\mathbb{R}$ of real numbers) but do not specify neither base of the computer arithmetics, nor a format of numbers representation. Incrementality means that we start with the most straightforward specification of the simplest case to verify the algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetics. We call our approach combined because we start with manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for a manual verification of the algorithm in computer arithmetics, and finish with a computer-aided validation of the manual proofs with a proof-assistant system (to avoid appeals to “obviousness” that are common in human-carried proofs). In the paper, we apply our platform-independent incremental combined approach to specification and verification of the standard Mathematical square root function. Currently a computer-aided validation was carried for correctness (consistency) of our fix-point arithmetics and for the existence of a look-up table with the initial approximations of the square roots for fix-point numbers.

Détail

Keywords: fix-point numbers, floating-point numbers, computer arithmetic, formal verification, partial and total correctness, Hoare triples, Floyd verification method of inductive assertions, exact function, square root function, Newton–Raphson method, look-up table.