Shmuel Katz
Abstract
Most present systems for verification of computer programs are incomplete in that intermediate inductive assertions must be provided manually by the user, termination is not proven, and incorrect programs are not treated. As a unified solution to these problems, this paper suggests conducting a logical analysis of programs by using invariants which express what is actually occurring in the program.
The first part of the paper is devoted to techniques for the automatic generation of invariants. The second part provides criteria for using the invariants to check simultaneously for correctness (including termination) or incorrectness. A third part examines the implications of the approach for the automatic diagnosis and correction of logical errors.
- 1 Allen, F.E. A basis for program optimization. Proc. IFIP Cong. 71, Vol. 1, North-Holland Pub. Co., Amsterdam, 1971, pp. 385-390.Google Scholar
- 2 Cooper, D.C. Programs for mechanical program verification. Machine Intelligence 6, American Elsevier, New York, 1971, pp. 43-59.Google Scholar
- 3 Caplain, M. Finding invariant assertion for proving programs. Proc. Int. Conf. on Reliable Software, Los Angeles, Calif., April 1975. Google ScholarDigital Library
- 4 Dahl, O.J., Dijkstra, E.W., and Hoare, C.A.R. Structured Programming. Academic Press, New York, 1972. Google ScholarDigital Library
- 5 Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dept. of Computer Sci., U. of California, Berkeley, June 1973.Google Scholar
- 6 Elspas, B., Levitt, K.N., and Waldinger, R.J. An interactive system for the verification of computer programs. Research Rep., SRI, Menlo Park, Calif., Sept. 1973.Google Scholar
- 7 Elspas, B. The semiautomatic generation of inductive assertions for proving program correctness. Research Rep., SRI, Menlo Park, Calif., July 1974.Google Scholar
- 8 Floyd, R.W. Assig.ning meaning to programs. Proc. Symp. in Appl. Math., Vol. 19, J.T. Schwartz (Ed.), Amer. Math. Soc., Providence, R.I., 1967, pp. 19-32.Google Scholar
- 9 Floyd, R.W. Towards interactive design of correct programs. Proc. IFIP Cong., Vol. 1, North-Holland Pub. Co., Amsterdam, 1971, pp. 7-10.Google Scholar
- 10 German, S. M. A program verifier that generates inductwe assertions. B.A. Th., Harvard U., May 1974.Google Scholar
- 11 Greff, I., and Waldmger, R. A more mechanical heuristic approach to program verification. Proc. Int. Symp. on Programming, Paris, April 1974, pp. 83-90. Google ScholarDigital Library
- 12 Hoare, C.A.R. An axiomatic basis of computer programming. Comm. ACM 12, 10 (Oct. 1969), 576-580, 583. Google ScholarDigital Library
- 13 Hoare, C.A.R. Proof of a program: FIND. Comm. ACM 14, 1 (Jan. 1971), 39-45. Google ScholarDigital Library
- 14 Katz, S.M., and Manna, Z. A heuristic approach to program verification. Proc. 3rd Int. Conf. on Artificial Intelligence, Stanford U., Aug. 1973, pp. 500-512.Google ScholarDigital Library
- 15 Katz, S.M., and Manna, Z. Towards automatic debugging of programs. Proc. Int. Conf. on Reliable Software, Los Angeles, Calif., April 1975, pp. 143-155. Google ScholarDigital Library
- 16 Katz, S.M., and Manna, Z. A closer look at termination. Acta InJormatica, to appear.Google Scholar
- 17 King, J. A program verifier. Ph.D. Th., Dep. of Computer Sci., Carnegie-Mellon U., Pittsburgh, Pa., 1969. Google ScholarDigital Library
- 18 King, J. A verifying compiler. In Debugging Techniques in Large Systems, Randall Rustin (Ed.), Prentice-Hall, Englewood Cliffs, N.J. 1970, pp. 17-39.Google Scholar
- 19 Knuth, D.E. The Art of Computer Programming, Vol. I, Fundamental Algorithms. Addison-Wesley, Reading, Mass. 1968. Google ScholarDigital Library
- 20 Manna, Z. The correctness of programs. J. Computer and System Sci., 3, 2 (May 1969), 119-127.Google Scholar
- 21 Manna, Z. Mathematical Theory of Computation. McGraw- Hill, New York, 1974. Google ScholarDigital Library
- 22 Maurer, W.D. The theory and practice of algorithm verification. ERL-M315, U. of California, Berkeley, Aug. 1973.Google Scholar
- 23 Misra, J. Relations uniformly conserved by a loop. Proc. Int. Symp. on Proving and Improving Programs, Arc et Senans, France, July 1975, pp. 71-80.Google Scholar
- 24 Moriconi, M.S. Towards the interactive synthesis of assertions. Research Rep., U. of Texas at Austin, Oct. 1974.Google Scholar
- 25 Sussman, G.J. A computational model of skill acquisition. Ph.D. Th., MIT, Cambridge, Mass., Aug. 1973.Google Scholar
- 26 Sites, R.L. Proving that computer programs terminate cleanly. Ph.D. Th., Dep. of Computer Science, Stanford U., STAN-CS-74- 418, May 1974. Google ScholarDigital Library
- 27 Waldinger, R. and Levitt, K.N. Reasoning about programs. Artificial Intelligence 5 (1974), 235-316.Google ScholarCross Ref
- 28 Wegbreit, B. The synthesis of loop predicates. Comm. ACM 17, 2 (Feb. 1974), 102-112. Google ScholarDigital Library
- 29 Wensley, J.H. A class of non-analytical interactive processes. Computer J., 1 (1958), 163-167.Google ScholarCross Ref
Index Terms
- Logical analysis of programs
Recommendations
Towards automatic debugging of programs
International Conference on Reliable SoftwareWe present the germ of an idea for automatically correcting logical errors in programs by manipulating the invariants of the program. An invariant tree is defined, and we show how it can be used to change the program in order to guarantee correctness.
...
Towards automatic debugging of programs
Proceedings of the international conference on Reliable softwareWe present the germ of an idea for automatically correcting logical errors in programs by manipulating the invariants of the program. An invariant tree is defined, and we show how it can be used to change the program in order to guarantee correctness.
...
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural ...
Comments