Platform-Independent Specification and Verification of the Standard Mathematical Square Root Function

The aim of the Platform-Independent Approach to Formal Specification and Verification of Standard Mathematical Functions project is the development of an incremental combined approach to specification and verification of standard mathematical functions like sqrt, cos, sin, etc. The term “platform-independence” means that we attempt to design a relatively simple axiomatization of computer arithmetic in terms of real arithmetic (i.e., the arithmetic of the field ℝ of real numbers), but do not specify either the base of the computer arithmetic or the format of the representation of numbers. The incrementality means that we start with the most straightforward specification of the simplest algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetic. We call our approach combined because we start with consideration of a “basic” case, the manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for the manual verification of the algorithm in computer arithmetic, 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. By now, the computer-aided validation of the developed algorithms has been carried out only partially to prove, using the ACL2 system, the correctness (consistency) of our fixed-point arithmetic and the existence of a look-up table with the initial approximations of the square roots for fixed-point numbers.