Improving and refining programs by program manipulation

ABSTRACT

By manipulating programs to reorganize the way they compute their results, it is possible to improve program performance in certain desirable directions. Further, using certain laws of exchange, it is possible to transform concise, abstract, high-level programs into efficient, concrete , underlying representations. This paper explores the notion of using source-to-source transformations interactively as a basis for an approach to program improvement and refinement. Examples of program manipulation are presented that convey both the flavor of the approach and its requirements.

REFERENCES

• 1: Niklaus Wirth, Program development by stepwise refinement, Communications of the ACM, v.14 n.4, p.221-227, April 1971 [doi>10.1145/362575.362577]
• 2: Ole Johan Dahl, Structured Programming, Academic Press, Inc., Orlando, FL, 1972
• 3: Marvin Schaefer, A mathematical theory of global program optimization (Prentice-Hall series in automatic computation), Prentice-Hall, Inc., Upper Saddle River, NJ, 1973
• 4: Allen, F.E., and Cocke,J., A Catalogue of Optimizing Transformations, in Design and Optimization of Compilers, (R. Rustin ed.), Prentice-Hall, Englewood Cliffs, N.J., (1972), pp. 1-30.
• 5: Alfred V. Aho , Jeffrey D. Ullman, Theory of Parsing, Translation and Compiling, Prentice Hall Professional Technical Reference, 1973
• 6: Allen, J.C., and Luckham, D.C., An Interactive Theorem Proving Program, Machine Intelligence 5, (Meltzer, B., and Michie, D. eds), American Elsevier, New York, (1970), 321-336.
• 7: Cheatham, T.E., and Wegbreit, B., A Laboratory for the Study of Automatic Programming, Proc. AFIPS Spring Joint Computer Conference, Vol. 40, AFIPS Press, Montvale, N.J., (1972), 11-21.
• 8: London, R.L., Proving Programs Correct: Some Techniques and Examples, BIT 10(1970), 168-182.
• 9: Waldinger, R.J., and Levitt, K.N., Reasoning about Programs, Tech. note 86, A.I. Center, Stanford Research Institute, Menlo Park, Cal., (October 1973).
• 10: 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]
• 11: Green, C., Application of Theorem Proving to Problem Solving, Proc. IJCAI 1, Washington, D.C., (1969), 219-239.
• 12: 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]
• 13: James Richard Low, Automatic coding: choice of data structures., 1974
• 14: J. T. Schwartz, Automatic data structure choice in a language of very high level, Communications of the ACM, v.18 n.12, p.722-728, Dec. 1975 [doi>10.1145/361227.361235]
• 15: Hewitt, C., and Smith, B., Towards a Programming Apprentice, Working Paper 90, A.I. Lab., MIT, Cambridge, Mass. (Jan. 1975).
• 16: Donald E. Knuth, Structured Programming with go to Statements, ACM Computing Surveys (CSUR), v.6 n.4, p.261-301, Dec. 1974 [doi>10.1145/356635.356640]
• 17: Ingalls, D., The Execution Time Profile as a Programming Tool, in Design and Optimization of Compilers, (Rustin, R. ed.), Prentice-Hall, Englewood Cliffs, N.J., (1972), pp. 107-128.
• 18: Knuth, D.E., An Empirical Study of FORTRAN Programs, Software—Practice and Experience 1 (1971), 105-133.
• 19: 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]
• 20: Beckman, L., Haraldson, A., Oskarsson, O., and Sandewall, E., A Partial Evaluator, and Its Use as a Programming Tool, DLU 74/34, DatalogiLaboratoriet, Inst. f. Informationsbehandling, Uppsala University, Uppsala, Sweden,(Nov. 1974).
• 21: David B. Loveman, Program improvement by source to source transformation, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.140-152, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811548]
• 22: Standish, T., Harriman, D., Kibler, D., and Neighbors, J., The Irvine Program Transformation Catalogue, Computer Science Department, U.C. Irvine, Irvine, Cal., (Jan. 1976).
• 23: Reynolds, J.C., Transformational Systems and the Algebraic Structure of Atomic Formulas, Machine Intelligence 5, (1970), 135-151.
• 24: Plotkin, G.D., A Note on Inductive Generalization, Machine Intelligence 5, (1970),153-163.
• 25: Standish, T., Kibler, D., Neighbors, J., and Winkler, T., Verifying Source-to-Source Transformations, (in preparation).
• 26: Standish, T.A., Arcturus: An Interactive Program Manipulation System, (in preparation).

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.0 General

General Terms:
Algorithms, Performance, Theory, Verification