The mathematical concept of real numbers is much richer than the double precision numbers widely used as their implementation on a computer. The field of 'exact real arithmetic' tries to combine the elegance and correctness of the mathematical theories with the speed of double precision hardware, as far as possible. In this paper, we describe an ongoing approach using the specification language ACSL, the tool suite Frama-C (with why and jessie) and the proof assistant Coq to verify central aspects of the iRRAM software package, which is known to be a fast C++ implementation of 'exact' reals numbers.
展开▼
