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 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.

REFERENCES

• 1: Robert S. Boyer , Bernard Elspas , Karl N. Levitt, SELECT—a formal system for testing and debugging programs by symbolic execution, Proceedings of the international conference on Reliable software, p.234-245, April 21-23, 1975, Los Angeles, California
• 2: Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
• 3: Burstall, R.M. Proving properties of programs by structural induction. Comptr. J. 12 (1969), 41-48.
• 4: Clarke, L. A system to generate test data and symbolically execute programs. 1EEE Trans. Software Eng. 2, 3 (1976), 227-231.
• 5: Dabl, O.-J., Dijkstra, E.W., and Hoare, C.A.R. Structured Programming. Academic Press, London and New York, 1972.
• 6: Floyd, R.W. Assigning meanings to programs. Proceedings of a Symposium in Applied Mathematics, Vol. 19, J. T. Schwartz, Ed., Amer. Math. Soc., 1967, pp. 19-32.
• 7: John B. Goodenough , Susan L. Gerhart, Toward a theory of test data selection, Proceedings of the international conference on Reliable software, p.493-510, April 21-23, 1975, Los Angeles, California
• 8: Peter Henderson, Finite state modelling in program development, Proceedings of the international conference on Reliable software, p.221-227, April 21-23, 1975, Los Angeles, California
• 9: Hoare, C.A.R. Proof of correctness of data representation. Acta lnformatica 1, 4 (1972), 271-281.
• 10: Howden, W.E. Reliability of the path analysis testing strategy. 1EEE Trans. Software Eng. 2, 3 (1976), 208-214.
• 11: Katz, S.M., and Manna, Z. Logical analysis of programs. The Weizmann Inst. of Sci., 1974.
• 12: James C. King, A new approach to program testing, Proceedings of the international conference on Reliable software, p.228-233, April 21-23, 1975, Los Angeles, California
• 13: Liskov, B.H., and Zilles, S.N. Specification techniques for data abstractions. IEEE Trans. on Software Eng. 1, 1 (March 1975), 7-19.
• 14: Ralph L. London, A view of program verification, Proceedings of the international conference on Reliable software, p.534-545, April 21-23, 1975, Los Angeles, California
• 15: Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Communications of the ACM, v.16 n.8, p.491-502, Aug. 1973 [doi>10.1145/355609.362336]
• 16: E. F. Miller, Jr. , R. A. Melton, Automated generation of testcase datasets, Proceedings of the international conference on Reliable software, p.51-58, April 21-23, 1975, Los Angeles, California
• 17: Robinson, L., and Levitt, K. Proof techniques for hierarchically structured programs. Standord Res. Inst., Menlo Park, Calif., 1975.
• 18: Michel Sintzoff, Calculating properties of programs by valuations on specific models, Proceedings of ACM conference on Proving assertions about programs, p.203-207, January 06-07, 1972, Las Cruces, New Mexico, United States
• 19: Sites, R. Proving that computer programs terminate cleanly. TR STAN-CS-74-418, Stanford, U., Stanford, Calif., 1974.
• 20: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Design, Performance, Reliability, Theory, Verification

Keywords:
inductive assertions, program testing, program verification, recursive programs, symbolic evaluation