R. M. Burstall
Abstract
A system of rules for transforming programs is described, with the programs in the form of recursion equations. An initially very simple, lucid, and hopefully correct program is transformed into a more efficient one by altering the recursion structure. Illustrative examples of program transformations are given, and a tentative implementation is described. Alternative structures for programs are shown, and a possible initial phase for an automatic or semiautomatic program-manipulation system is indicated.
- 1 AualN, R Some generahsatlon heuristics m proofs by reduction Proc IRIA Symp Proving and Improving Programs, Arc-et-Senans, France, 1975, pp 197-208Google Scholar
- 2 BORER, R S , AND MOORE, JS Proving theorems about LISP functions J ACM 22, 1 (Jan 1975), 129- 144 Google Scholar
- 3 CHEATnAM, T E JR , AND WEGBREIT, B A laboratory for the study of automating programming Proc AFIPS 1972 SjCC; Vol 40, AFIPS Press, Montvale, N.J., pp 11-21Google Scholar
- 4 COURCELLE, B , AND VUILLEMIN, J Semantics and axtomattcs of a simple recurswe language Proc Sixth Annual ACM Symp Theory of Comptg , 1974, pp 13-26 Google Scholar
- 5 DARLINGTON~ J A semantm approach to automatic program tmprovement Ph D Th, Dep Artif lntel, U of Edinburgh, Edinburgh, 1972Google Scholar
- 6 DARLINGTON, J , AND BURSTALL, R M A system which automatically improves programs Proc Third Int Joint Conf on Artlf Intel , Stanford, Cahf , 1973, pp. 479-485. (To appear m Acta Informattca, 1976.)Google Scholar
- 7 DARLINGTON, J Application of program transformation to program synthesis Proc IRIA Symp Proving and Improving Programs, Arc-et-Senans, France. 1975. pp 133-144Google Scholar
- 8 FLOYD, R.W Algorithm 245, TREESORT 3 Comm ACM 7, 12 (Dec 1964), 701-702 Google Scholar
- 9 GERUART, S L Correctness-preserving program transformauons Conf Rec Second Symp Prlnoples of Programming Languages, Palo Alto, Calif, 1975, pp 54-66 Google Scholar
- 10 HOARE, C A R Proof of correctness of data representations Acta Informat~ca 1 (1972), 271-278Google Scholar
- 11 KNUTH, D E Structured programming w~th go to statements ACM Computmg Surveys 6, 4 (1974), 261-301 Google Scholar
- 12 MANNA, Z., AND WALDINGER, R Knowledge and reasoning m program synthesis Arttf Intel J 6, 2 (1975), 175-208Google Scholar
- 13 Moo~E, JS Introducing Iteration into the pure LISP theorem prover CSL-74-3, Xerox Palo Alto Res Ctr, Palo Alto, Callf, 1975Google Scholar
- 14 PLOTKIN, G Budding in equational theories Machme lntelhgence 7, B Meltzer and D. Michle, Eds , Edinburgh U Press, Edinburgh, 1972, pp 73-90Google Scholar
- 15 ToPoR, R W Interactive program verification using virtual programs Ph D Th, Dep Artff Intel, U of Edinburgh, Edinburgh, 1975Google Scholar
Index Terms
- A Transformation System for Developing Recursive Programs
Recommendations
Some transformations for developing recursive programs
International Conference on Reliable SoftwareThe paper describes a system of rules for transforming programs, the programs being in the form of recursion equations. The idea is to start with a very simple, lucid and hopefully correct program, then to transform it into a more efficient one by ...
Some transformations for developing recursive programs
Proceedings of the international conference on Reliable softwareThe paper describes a system of rules for transforming programs, the programs being in the form of recursion equations. The idea is to start with a very simple, lucid and hopefully correct program, then to transform it into a more efficient one by ...
Applications of the TAMPR transformation system
IW-FM'98: Proceedings of the 2nd Irish conference on Formal MethodsIn this paper we present an overview of the uses of the TAMPR transformation system and present experience with using transformation in industrial applications. TAMPR is a fully automatic, rewrite-rule based program transformation system. From its ...
Comments