Test data as an aid in proving program correctness
- 1 May 1978
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 21 (5) , 368-375
- https://doi.org/10.1145/359488.359495
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 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.Keywords
This publication has 12 references indexed in Scilit:
- Toward a theory of test data selectionPublished by Association for Computing Machinery (ACM) ,1975
- A new approach to program testingPublished by Association for Computing Machinery (ACM) ,1975
- Automated generation of testcase datasetsPublished by Association for Computing Machinery (ACM) ,1975
- SELECT---a formal system for testing and debugging programs by symbolic executionPublished by Association for Computing Machinery (ACM) ,1975
- Proving Theorems about LISP FunctionsJournal of the ACM, 1975
- The synthesis of loop predicatesCommunications of the ACM, 1974
- Inductive methods for proving properties of programsCommunications of the ACM, 1973
- Calculating properties of programs by valuations on specific modelsPublished by Association for Computing Machinery (ACM) ,1972
- Proving Properties of Programs by Structural InductionThe Computer Journal, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967