Formal program testing

ABSTRACT

This paper proposes a practical alternative to program verification -- called formal program testing -- with similar, but less ambitious goals. Like a program verifier, a formal testing system takes a program annotated with formal specifications as input, generates the corresponding verification conditions, and passes them through a simplifier. After the simplification step, however, a formal testing system simply evaluates the verification conditions on a representative set of test data instead of trying to prove them. Formal testing provides strong evidence that a program is correct, but does not guarantee it. The strength of the evidence depends on the adequacy of the test data.

REFERENCES

• 1: 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]
• 2: {Boyer and Moore 79} Boyer, R. S., and Moore, J S. A Computational Logic, Academic Press, New York, 1979.
• 3: {Brand 76} Brand, D.; "Proving Programs Incorrect," Proceedings Third International Colloquium on Automata, Languages and Programming, Edinburgh U. Press, Edinburgh, 1976, pp. 201-227.
• 4: Daniel Brand, Path Calculus in Program Verification, Journal of the ACM (JACM), v.25 n.4, p.630-651, Oct. 1978 [doi>10.1145/322092.322103]
• 5: Timothy A. Budd , Richard A. DeMillo , Richard J. Lipton , Frederick G. Sayward, Theoretical and empirical studies on using program mutation to test the functional correctness of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.220-233, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567468]
• 6: {Cartwright 76a} Cartwright, R. S.; "User-Defined Data Types as an Aid to Verifying LISP Programs," Proceedings Third International Colloquium on Automata, Languages and Programming, Edinburgh U. Press, Edinburgh, 1976, pp. 228-256.
• 7: {Cartwright 76b} Cartwright, R. S.; A Practical Formal Semantic Definition and Verification System for TYPED LISP, Stanford Artificial Intelligence Laboratory Memo AIM-296, Stanford University, 1976.
• 8: Robert Cartwright, A constructive alternative to axiomatic data type definitions, Proceedings of the 1980 ACM conference on LISP and functional programming, p.46-55, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802789]
• 9: {Earley 73} Earley, J.; "High Level Operations in Automatic Programming," Computer Science Department, Technical Report 22, University of California, Berkeley, 1973.
• 10: {Earley 74} Earley, J.; "High Level Iterators and a Method for Automatically Designing Data Structure Representation," Electronics Research Laboratory, Memorandum No. ERL-M425, University of California, Berkeley, 1974.
• 11: Susan L. Gerhart, Correctness-preserving program transformations, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.54-66, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512983]
• 12: J. A. Goguen , J. W. Thatcher , E. G. Wagner , J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM (JACM), v.24 n.1, p.68-95, Jan. 1977 [doi>10.1145/321992.321997]
• 13: {Guttag and Horning 78} Guttag, J. V. and J J. Horning; "The Algebraic Specification of Abstract Data Types," Acta Informatica 10, pp. 27-52.
• 14: Friedrich W. von Henke , David C. Luckham, Automatic program verification III: a methodology for verifying programs., Stanford University, Stanford, CA, 1974
• 15: {Hoare 72} Hoare, C. A. R.; "Proofs of Correctness of Data Representation," Acta Informatica 1, 271-281.
• 16: {Hoare 75} Hoare, C. A. R. "Recursive Data Structures," International Journal of Comment and Information Sciences 4,2, pp. 105-132.
• 17: {Igarashi, London and Luckham 75} Igarashi, S., London; R. L., and Luckham, D. C.; "Automatic Program Verification I: Logical Basis and Its Implementation," Acta Informatica 4, pp. 145-182.
• 18: {Kennedy and Schwartz 75} Kennedy, K. and Schwartz, J. T, "An Introduction to the Set Theoretical Language SETL," J. Comptr. and Math. with Applications 1 (1975), pp. 97-119.
• 19: {Liskov and Zilles 75} Liskov, B. and S. Zilles; "Specification Techniques for Data Abstractions," IEEE Transactions on Software Engineering, Vol. SE-1, pp. 7-19.
• 20: {Liskov and Berzins 80} Liskov, B. and V. Berzins; "An Appraisal of Program Specifications," in Research Directions in Software Technology, P. Wegner (ed.), MIT Press, pp. 276-302.
• 21: David C. Luckham , Norihisa Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.226-244, Oct. 1979 [doi>10.1145/357073.357078]
• 22: {McCarthy 63} McCarthy, J.; "A Basis for a Mathematical Theory of Computation," in Computer Programming and Formal Systems, Braffort and Hirschberg, eds., North-Holland, 1963.
• 23: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 24: {Schwartz 79} Schwartz, J.; Personal communication.
• 25: David H D Warren , Luis M. Pereira , Fernando Pereira, Prolog - the language and its implementation compared with Lisp, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.109-115, August 15-17, 1977