Test data as an aid in proving program correctness
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 the process of providing correctness, this method simplifies the process of providing accurate specification for a program. The applicability of this technique to procedures and recursive programs is demonstrated.