Abstract
The current approach for testing a program is, in principle, quite primitive. Some small sample of the data that a program is expected to handle is presented to the program. If the program produces correct results for the sample, it is assumed to be correct. Much current work focuses on the question of how to choose this sample. We propose that a program can be more effectively tested by executing it "symbolically." Instead of supplying specific constants as input values to a program being tested, one supplies symbols. The normal computational definitions for the basic operations performed by a program can be expanded to accept symbolic inputs and produce symbolic formulae as output. If the flow of control in the program is completely independent of its input parameters, then all output values can be symbolically computed as formulae over the symbolic inputs and examined for correctness. When the control flow of the program is input dependent, a case analysis can be performed producing output formulae for each class of inputs determined by the control flow dependencies. Using these ideas, we have designed and implemented an interactive debugging/testing system called EFFIGY.
- 1 Deutsch, L.P. An interactive program verifier, Ph.D. dissertation, Dept. Comp. Sci., Univ. of Calif., Berkeley CA., May 1973.Google Scholar
- 2 Floyd, R.W. Assigning meanings to programs, Proc. Symp. Appl. Math., Amer. Math. Soc., vol. 19, pp. 19-32, 1967.Google ScholarCross Ref
- 3 Good, D.I. Toward a man-machine system for proving program correctness, Ph.D. dissertation, Comp. Sci. Dept., Univ. of Wisc., Madison, Wisc., June 1970. Google ScholarDigital Library
- 4 King, J.C. and Floyd, R.W. An interpretation oriented theorem prover over integers, Journal of Comp. and Sys. Sci., vol. 6, no. 4, August 1972, pp. 305-323.Google ScholarDigital Library
- 5 King, J.C. A program verifier, IFIP Congress 71 Proc., Aug. 1971, pp. 235-249.Google Scholar
- 6 Sites, R.L. Proving that computer programs terminate cleanly, Ph.D. dissertation, Comp. Sci. Dept., Stanford Univ., Stanford, CA., May 1974. Google ScholarDigital Library
- 7 Topor, R. W. Interactive program verification using virtual programs, Ph.D. dissertation, Department of Artificial Intelligence, University of Edinburgh, Edinburgh, Scotland, February 1975.Google Scholar
- 8 Topor, R. W. and Burstall, R. M. Verification of programs by symbolic execution - progress report, unpublished report, Dept. of Mach. Intelligence, Univ. of Edinburgh, Edinburgh, Scotland, December 1973.Google Scholar
Index Terms
- A new approach to program testing
Recommendations
Symbolic execution and program testing
This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program (e.g. numbers) one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be ...
A new approach to program testing
Proceedings of the international conference on Reliable softwareThe current approach for testing a program is, in principle, quite primitive. Some small sample of the data that a program is expected to handle is presented to the program. If the program produces correct results for the sample, it is assumed to be ...
Compiler testing via symbolic interpretation
ACM '76: Proceedings of the 1976 annual conferenceA method for compiler testing using symbolic interpretation is presented. This method is a cross between program proving and program testing. It is useful in demonstrating that programs are correctly translated from a high level language to a low level ...
Comments