Logical analysis of programs

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.

REFERENCES

• 1: Allen, F.E. A basis for program optimization. Proc. IFIP Cong. 71, Vol. 1, North-Holland Pub. Co., Amsterdam, 1971, pp. 385-390.
• 2: Cooper, D.C. Programs for mechanical program verification. Machine Intelligence 6, American Elsevier, New York, 1971, pp. 43-59.
• 3: Michel Caplain, Finding Invariant assertions for proving programs, Proceedings of the international conference on Reliable software, p.165-171, April 21-23, 1975, Los Angeles, California
• 4: Ole Johan Dahl, Structured Programming, Academic Press, Inc., Orlando, FL, 1972
• 5: Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dept. of Computer Sci., U. of California, Berkeley, June 1973.
• 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.
• 7: Elspas, B. The semiautomatic generation of inductive assertions for proving program correctness. Research Rep., SRI, Menlo Park, Calif., July 1974.
• 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.
• 9: Floyd, R.W. Towards interactive design of correct programs. Proc. IFIP Cong., Vol. 1, North-Holland Pub. Co., Amsterdam, 1971, pp. 7-10.
• 10: German, S. M. A program verifier that generates inductwe assertions. B.A. Th., Harvard U., May 1974.
• 11: Irene Greif , Richard J. Waldinger, A more mechanical approach to program verification, Programming Symposium, Proceedings Colloque sur la Programmation, p.109-119, April 09-11, 1974
• 12: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 13: C. A. R. Hoare, Proof of a program: FIND, Communications of the ACM, v.14 n.1, p.39-45, Jan. 1971 [doi>10.1145/362452.362489]
• 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.
• 15: Shmuel Katz , Zohar Manna, Towards automatic debugging of programs, Proceedings of the international conference on Reliable software, p.143-155, April 21-23, 1975, Los Angeles, California
• 16: Katz, S.M., and Manna, Z. A closer look at termination. Acta InJormatica, to appear.
• 17: James Cornelius King, A program verifier, 1970
• 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.
• 19: Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 20: Manna, Z. The correctness of programs. J. Computer and System Sci., 3, 2 (May 1969), 119-127.
• 21: Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
• 22: Maurer, W.D. The theory and practice of algorithm verification. ERL-M315, U. of California, Berkeley, Aug. 1973.
• 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.
• 24: Moriconi, M.S. Towards the interactive synthesis of assertions. Research Rep., U. of Texas at Austin, Oct. 1974.
• 25: Sussman, G.J. A computational model of skill acquisition. Ph.D. Th., MIT, Cambridge, Mass., Aug. 1973.
• 26: Richard Lee Sites, Proving that computer programs terminate cleanly., 1974
• 27: Waldinger, R. and Levitt, K.N. Reasoning about programs. Artificial Intelligence 5 (1974), 235-316.
• 28: 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]
• 29: Wensley, J.H. A class of non-analytical interactive processes. Computer J., 1 (1958), 163-167.

INDEX TERMS

Keywords:
automatic debugging, correctness, incorrectness, invariants, logical analysis, program verification, termination