Test Data as an Aid in Proving Program Correctness

Abstract

Proofs of program correctness tend to be long and tedious whereas testing, though useful in detecting errors, usually does not guarantee correctness. This paper introduces a technique whereby test data can be used in proving program correctness. In addition to simplifying certification of correctness, this method simplifies the process of providing specifications for a program. The applicability of this technique to procedures, recursive programs, and modular programs is demonstrated.