Verifying asymptotic correctness

A notion of asymptotic correctness for programs involving real number computation is examined. Roughly speaking, a program P asymptotically computes the function f if for every input x the output of P, as a function of the precision of the machine on which P is run, converges to f(x). In particular, if P does not mention reals, then asymptotic correctness is just correctness. Asymptotic correctness says nothing about how precise the machine needs to be to get a particular degree of accuracy, only that for any positive ∈ and any x, if P is run on a precise enough machine, then the output of the program will be within ∈ of f(x). It is this fact that makes the notion interesting for verification. Even though the asymptotic correctness of a program will not specify the behavior of the program on any particular machine, it will filter out certain types of logical errors which can occur when using infinitary data types and programming with them as if they were modeled ideally on the computer