An improved program-synthesizing algorithm and its correctness
- 1 April 1974
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 17 (4), 211-217
- https://doi.org/10.1145/360924.360967
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.Keywords
This publication has 3 references indexed in Scilit:
- Toward automatic program synthesisCommunications of the ACM, 1971
- Application of Theorem Proving to Problem SolvingPublished by Defense Technical Information Center (DTIC) ,1969
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965