Access Restriction

Author Waldinger, R. J. ♦ Lee, R. C. T. ♦ Chang, C. L.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Primitive resolutions ♦ Theorem proving ♦ Program-synthesizing algorithms ♦ Consequence finding
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.
Description Affiliation: National Institutes of Health, Bethesda, MD (Lee, R. C. T.; Chang, C. L.) || Stanford Research Institute, Menlo Park, CA (Waldinger, R. J.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 17
Issue Number 4
Page Count 7
Starting Page 211
Ending Page 217

Open content in new tab

   Open content in new tab
Source: ACM Digital Library