Verification of Numerical Algorithms

The following strategy is suggested for specification and proof: (1) Defer the construction of a formal program specification with respect to I/O assertions unit the correctness of the program with respect to an abstract mathematical model of program intent is demonstrated. (2) Prove that an abstract machine (using infinite precision arithmetic) would compute that object exactly. (3) Prove that the computational sequences of arithmetic operations that occur in the abstract machine must be precisely the same at every step as those occurring on an actual machine (with finite precision arithmetic), executing the same program. (4) Use a Verification Conditions VC-generator that knows about the semantics of arithmetic operations to annotate the program with assertions that bound (or in some circumstances estimate) the difference between the actual machine state variables and the corresponding ones of the abstract machine. Construct the formal program specification by combining the verification conditions into theorems about computational error that can be proved with mechanical assistance.