Verified real computation

Abstract

Computing with infinite data such as real numbers cannot be performed exactly on a Turing machine. Instead, real numbers are treated as an infinite sequence of approximations. Computing a real function means that a Turing machine converts approximations to the argument into approximations of the value, according to Computable Analysis. [Brattka&Hertling’98] have suggested an equivalent but more practical model of computation over the reals: the feasible real-RAM. Based on this fundamental idea, the iRRAM library for C++ has been developed as an imperative programming language which supports abstract datatypes with exact and multivalued semantics. In this dissertation, we extend Floyd-Hoare logic to formally verify correctness of such algorithms. A set of inference rules is suggested as a systematic framework for program verification. We also consider the diagonalization of complex self--adjoint matrices with a particular emphasis on the degenerate cases, which in general are ill-posed and in fact provably uncomputable. Employing a Recursive Analysis, we have designed, implemented and evaluated several reliable algorithms on iRRAM which can compute some orthonormal basis of eigenvectors, in the sense of output approximation, up to any desired precision - provided that, in addition to approximations to the d(d+1)/2 matrix' entries, its number of distinct eigenvalues k is known/provided.