article

Free access

The automatic synthesis of recursive programs

Authors:

Zohar Manna,

Richard WaldingerAuthors Info & Claims

ACM SIGART Bulletin, Issue 64

Pages 29 - 36

https://doi.org/10.1145/872736.806929

Published: 01 August 1977 Publication History

PDF eReader

Abstract

We describe a deductive technique for the automatic construction of recursive programs to meet given input-output specifications. These specifications express what conditions the output of the desired program is expected to satisfy. The deductive technique involves transforming the specifications by a collection of rules, summoned by pattern-directed function invocation. Some of these transformation rules express the semantics of the subject domain; others represent more general programming techniques. The rules that introduce conditional expressions and recursive calls into the program are discussed in some detail.

The deductive techniques described are embedded in a running system called SYNSYS. This system accepts specifications expressed in high-level descriptive language and attempts to transform them into a corresponding LISP program. The transformation rules are expressed in the QLISP programming language. The synthesis of two programs performed by the system are presented.

This research was supported in part by the Advanced Research Projects Agency of the Department of Defense under Contract MDA903-76-C-0206, by the National Science Foundation under Grant DCR72-03737 A01, by the Office of Naval Research under Contracts N00014-76-C-0687 and N00014-75-C-0816; and by a grant from the United States-Israel Binational Science Foundation (BSF), Jerusalem, Israel.

The views and conclusions contained in this document are those of the authors and should not be interpreted as necessarily representing the official policies, either expressed or implied, of Stanford University, Stanford Research Institute, or the U.S. Government.

References

[1]

Barstow, D. R. and E. Kant {Oct. 1976},Observations on the interaction between coding and efficiency knowledge in the PSI program synthesis system, Proceedings of the Second International Conference on Software Engineering, San Francisco, Ca., pp. 19-31.

Digital Library

Google Scholar

[2]

Biedsoe, W. W., and M. Tyson {1977},Typing and proof by cases in program verification, in Machine Intelligence 8: Machine Representations of Knowledge, (E. W. Elcock and D. Michie, editors), Ellis Horwood, Edinburgh, Scotland (to appear).

Google Scholar

[3]

Boyer, R. S., and J S. Moore {Jan. 1975},Proving theorems about LISP functions, JACM, Vol. 22, No. 1, pp. 129-144.

Digital Library

Google Scholar

[4]

Burstall, R. M. and J. Darlington {April 1975},Some transformations for developing recursive programs, Proceedings of the International Conference on Reliable Software, Los Angeles, Ca., pp. 465-472.

Digital Library

Google Scholar

[5]

Darlington, J. {July 1975},Applications of program transformation to program synthesis, Colloques IRIA on Proving and Improving Programs, Arc et Senans, France, pp. 133-144.

Google Scholar

[6]

Dijkstra, E. W. {1976},A discipline of programming, Prentice-Hall, Englewood Cliffs, N. J.

Digital Library

Google Scholar

[7]

Manna, Z. and R. Waldinger {1975},Knowledge and reasoning in program synthesis, Artificial Intelligence, Vol. 6, No. 2, pp. 175-208.

Crossref

Google Scholar

[8]

Siklossy, L. {1974},The synthesis of programs from their properties, and the insane heuristic, Proceedings of the Third Texas Conference on Computing Systems, Austin, Texas.

Google Scholar

[9]

Waldinger, R. J. {1977},Achieveing several goals simultaneously, in Machine Intelligence 8: Machine Representations of Knowledge, (E. W. Elcock and D. Michie, editors), Ellis Horwood, Edinburgh, Scotland (to appear).

Google Scholar

[10]

Warren, D. H. D. {July 1976},Generating conditional plans and programs, Proceedings of Conference on Artificial Intelligence and Simulation on Behaviour, Edinburgh, Scotland, pp. 344-354.

Google Scholar

[11]

Wegbreit, B {Sept. 1975},Goal-directed program transformation, Research report, Xerox Research Center, Palo Alto, Ca.

Google Scholar

[12]

Wilber, B. M . {Mar. 1976},A QLISP reference manual, Technical note, Stanford Research Institute, Menlo Park, Ca.

Google Scholar

[13]

Wirth, N. {1976},Algorithms + data structures &equil; programs, Prentice-Hall Inc., Englewood Cliffs, N.J.

Digital Library

Google Scholar

Cited By

View all

Dershowitz NWaldinger R(2019)Zohar Manna (1939–2018)Formal Aspects of Computing10.1007/s00165-019-00500-431:6(643-660)Online publication date: Dec-2019
https://doi.org/10.1007/s00165-019-00500-4
Hesse W(1984)A systematics of software engineering: Structure, terminology and classification of techniquesProgram Transformation and Programming Environments10.1007/978-3-642-46490-4_11(97-125)Online publication date: 1984
https://doi.org/10.1007/978-3-642-46490-4_11
Sato T(2005)An equivalence preserving first order unfold/fold transformation systemAlgebraic and Logic Programming10.1007/3-540-53162-9_38(173-188)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-53162-9_38
Show More Cited By

Index Terms

The automatic synthesis of recursive programs

Recommendations

The automatic synthesis of recursive programs
Proceedings of the 1977 symposium on Artificial intelligence and programming languages

We describe a deductive technique for the automatic construction of recursive programs to meet given input-output specifications. These specifications express what conditions the output of the desired program is expected to satisfy. The deductive ...
The automatic synthesis of recursive programs
Proceedings of the 1977 symposium on Artificial intelligence and programming languages

We describe a deductive technique for the automatic construction of recursive programs to meet given input-output specifications. These specifications express what conditions the output of the desired program is expected to satisfy. The deductive ...
Automatic machine grading programs
ACM '64: Proceedings of the 1964 19th ACM national conference

In connection with introductory programming and numerical analysis courses at Stanford University, grading programs have been used intermittently since 1961. The original idea came from the TEACH routine devised at Carnegie Tech. by A. J. Perlis and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGART Bulletin Just Accepted

Proceedings of the 1977 symposium on Artificial intelligence and programming languages

August 1977

179 pages

ISSN:0163-5719

DOI:10.1145/872736

Issue’s Table of Contents

Proceedings of the 1977 symposium on Artificial intelligence and programming languages
August 1977
185 pages
ISBN:9781450378741
DOI:10.1145/800228
Chairman:
James Low

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1977

Published in SIGAI , Issue 64

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
348
Total Downloads

Downloads (Last 12 months)65
Downloads (Last 6 weeks)12

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Dershowitz NWaldinger R(2019)Zohar Manna (1939–2018)Formal Aspects of Computing10.1007/s00165-019-00500-431:6(643-660)Online publication date: Dec-2019
https://doi.org/10.1007/s00165-019-00500-4
Hesse W(1984)A systematics of software engineering: Structure, terminology and classification of techniquesProgram Transformation and Programming Environments10.1007/978-3-642-46490-4_11(97-125)Online publication date: 1984
https://doi.org/10.1007/978-3-642-46490-4_11
Sato T(2005)An equivalence preserving first order unfold/fold transformation systemAlgebraic and Logic Programming10.1007/3-540-53162-9_38(173-188)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-53162-9_38
Hogger C(2005)Goal-oriented derivation of logic programsMathematical Foundations of Computer Science 197810.1007/3-540-08921-7_74(267-276)Online publication date: 24-May-2005
https://doi.org/10.1007/3-540-08921-7_74
Partsch HSteinbrüggen R(1983)Program Transformation SystemsACM Computing Surveys10.1145/356914.35691715:3(199-236)Online publication date: 1-Sep-1983
https://dl.acm.org/doi/10.1145/356914.356917
Basu S(1980)A Note on Synthesis of Inductive AssertionsIEEE Transactions on Software Engineering10.1109/TSE.1980.2304606:1(32-39)Online publication date: 1-Jan-1980
https://dl.acm.org/doi/10.1109/TSE.1980.230460
(1978)BIBLIOGRAPHYPattern-Directed Inference Systems10.1016/B978-0-12-737550-2.50036-1(603-646)Online publication date: 1978
https://doi.org/10.1016/B978-0-12-737550-2.50036-1
Ulrich JMoll R(1977)Program synthesis by analogyACM SIGART Bulletin10.1145/872736.806928(22-28)Online publication date: 1-Aug-1977
https://dl.acm.org/doi/10.1145/872736.806928
Ulrich JMoll R(1977)Program synthesis by analogyACM SIGPLAN Notices10.1145/872734.80692812:8(22-28)Online publication date: 1-Aug-1977
https://dl.acm.org/doi/10.1145/872734.806928
Ulrich JMoll RLow J(1977)Program synthesis by analogyProceedings of the 1977 symposium on Artificial intelligence and programming languages10.1145/800228.806928(22-28)Online publication date: 15-Aug-1977
https://dl.acm.org/doi/10.1145/800228.806928
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations