Mechanical program analysis

ABSTRACT

One means of analyzing program performance is by deriving closed-form expressions for their execution behavior. This paper discusses the mechanization of such analysis, and describes a system, Metric, which is able to analyze simple Lisp programs and produce, for example, closed-form expressions for their running time expressed in terms of size of input. This paper presents the reasons for mechanizing program analysis, describes the operation of Metric, explains its implementation, and discusses its limitations.

REFERENCES

• 1: Beizer, B. Analytical techniques for the statistical evaluation of program running time. Proc. AFIPS 1970 FJCC, Vol. 37, AFIPS Press, Montvale, N.J., pp. 519-524.
• 2: Daniel G. Bobrow , Daniel L. Murphy, Structure of a LISP system using two-level storage, Communications of the ACM, v.10 n.3, p.155-159, March 1967 [doi>10.1145/363162.363185]
• 3: Cheatham, T.E., and Wegbreit, B. A laboratory for the study of automating programming. Proc. AFIPS 1972 SJCC, Vol. 40, AFIPS Press, Montvale, N.J., pp. 11-21.
• 4: John Cocke, Programming languages and their compilers: Preliminary notes, Courant Institute of Mathematical Sciences, New York University, 1969
• 5: Jacques Cohen , Carl Zuckerman, Two languages for estimating program efficiency, Communications of the ACM, v.17 n.6, p.301-308, June 1974 [doi>10.1145/355616.361015]
• 6: Green, C. Application of theorem-proving to problem solving. Proc. First Intemat. Joint Conf. on Artif. Intell., 1969, pp. 219-239.
• 7: Ingalls, D. The execution time profile as a programming tool. In Design and Optimization o f Compilers, R. Rustin, Ed., Prentice- Hall, Englewood Cliffs, N.J., 1972, pp. 107-128.
• 8: Knuth, D.E. An empirical study of FORTRAN programs. In Software-Practice and Experience, Vol. 1, 1971, pp. 105-133.
• 9: Donald Ervin Knuth, The Art of Computer Programming, 2nd Ed. (Addison-Wesley Series in Computer Science and Information, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1978
• 10: R. C. T. Lee , R. J. Waldinger , C. L. Chang, An improved program-synthesizing algorithm and its correctness, Communications of the ACM, v.17 n.4, p.211-217, April 1974 [doi>10.1145/360924.360967]
• 11: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 12: Zohar Manna , Richard J. Waldinger, Toward automatic program synthesis, Communications of the ACM, v.14 n.3, p.151-165, March 1971 [doi>10.1145/362566.362568]
• 13: Joel Moses, Algebraic simplification: a guide for the perplexed, Communications of the ACM, v.14 n.8, p.527-537, Aug. 1971 [doi>10.1145/362637.362648]
• 14: Alan G. Nemeth , Paul D. Dovner, User program measurement in a time-shared environment, Communications of the ACM, v.14 n.10, p.661-666, Oct. 1971 [doi>10.1145/362759.362810]
• 15: Proceedings of a symposium on very high level languages. SIGPLAN Notices, Vol. 9, No. 4 (Apr. 1974).
• 16: C. V. Ramamoorthy, Analysis of computational systems: Discrete Markov analysis of computer programs, Proceedings of the 1965 20th national conference, p.386-392, August 24-26, 1965, Cleveland, Ohio, United States [doi>10.1145/800197.806061]
• 17: R C. Bose , B Manvel, Introduction to combinatorial theory, John Wiley & Sons, Inc., New York, NY, 1984
• 18: Richard Lee Sites, Proving that computer programs terminate cleanly., 1974
• 19: Teitelman, W. bterlisp Reference Manual. Xerox Palo Alto Research Center, Palo Alto, Calif., 1974.
• 20: Weissman, C. Lisp 1.5 Primer. Dickenson Pub. Co., Belmont, Calif., 1967.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: LISP

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Languages, Performance

Keywords:
Lisp, algebraic manipulation, analysis of algorithms, analysis of programs, difference equations, execution behavior, execution time, generating functions, list processing, performance analysis, programming languages