An improved program-synthesizing algorithm and its correctness

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An improved program-synthesizing algorithm and its correctness

Full text

Pdf (504 KB)

Source

Communications of the ACM archive
Volume 17 , Issue 4 (April 1974) table of contents

Pages: 211 - 217

Year of Publication: 1974

ISSN:0001-0782

Authors

R. C. T. Lee	National Institutes of Health, Bethesda, MD
R. J. Waldinger	Stanford Research Institute, Menlo Park, CA
C. L. Chang	National Institutes of Health, Bethesda, MD

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 12, Citation Count: 10

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/360924.360967 What is a DOI?

ABSTRACT

An improved program-synthesizing algorithm based on the algorithm proposed by Waldinger and Lee in 1969 is given. In the old algorithm, the program-synthesizing problem is translated into a theorem-proving problem, and a program is obtained by analyzing a proof. For the improved algorithm, the analysis is not necessary, and a program is obtained as soon as the proof is completed. This is achieved by using a modified variable tracing mechanism invented by Green in 1969. The correctness of the improved algorithm is also proved; i.e. the program thus obtained always satisfies the specification.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Green, C. Application of theorem-proving to problem solving. Proc. First Internat. Joint Conf. on Artif. Intell., 1969, pp. 219-239.
	2	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]
	3	Nils J. Nilsson, Problem-Solving Methods in Artificial Intelligence, McGraw-Hill Pub. Co., 1971
	4	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	5	Slagle, J.R. Artificial httelligence, the Heuristic Programming Approach. McGraw-Hill, New York, 1971.
	6	Waldinger, R.J. Constructing programs automatically using theorem proving. Ph.D. Th. Carnegie-Mellon U., 1969.
	7	Waldinger, R.J., and Lee, R.C.T. PROW: A step toward automatic program writing. Proc. First Internat. Joint Conf. on Artif. Intell., 1969, pp. 241-252.

CITED BY 10

	Thomas A. Standish , Dennis F. Kibler , James M. Neighbors, Improving and refining programs by program manipulation, Proceedings of the annual conference, p.509-516, October 20-22, 1976, Houston, Texas, United States
	R. C. T. Lee , S. K. Chang, Structured programming and automatic program synthesis, ACM SIGPLAN Notices, v.9 n.4, p.60-70, April 1974
	Saumya K. Debray , Nai-Wei Lin, Cost analysis of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.5, p.826-875, Nov. 1993
	Ben Wegbreit, Mechanical program analysis, Communications of the ACM, v.18 n.9, p.528-539, Sept. 1975
	Alan W. Biermann, The use of examples in program construction and debugging, Proceedings of the 1975 annual conference, p.242-247, January 1975
	Sun Yong-qiang , Lu Ru-zhan , Bi Hua, Program synthesis based on Boyer-Moore theorem proving techniques, Proceedings of the 1985 ACM thirteenth annual conference on Computer Science, p.348-355, March 1985, New Orleans, Louisiana, United States
	Joe W. Duran, Heuristics for program synthesis using loop invariants, Proceedings of the 1978 annual conference, p.891-900, January 1978
	Yulia Korukhova, An approach to automatic deductive synthesis of functional programs, Annals of Mathematics and Artificial Intelligence, v.50 n.3-4, p.255-271, August 2007
	C. L. Chang, The NIH Heuristics laboratory, ACM SIGART Bulletin
	Jean Louis Lauriere, Toward efficiency trough generality, Proceedings of the 6th international joint conference on Artificial intelligence, p.519-521, August 20-23, 1979, Tokyo, Japan