Accession Number : AD0697041

Title :   CONSTRUCTING PROGRAMS AUTOMATICALLY USING THEOREM PROVING.

Descriptive Note : Doctoral thesis,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Waldinger,Richard J.

Report Date : MAY 1969

Pagination or Media Count : 109

Abstract : The paper describes a method by which programs may be constructed mechanically. The problem of writing a program is transformed into a theorem proving task. The specifications for the program are used to construct a theorem, the theorem is proved, and the program is derived from the proof of the theorem. The specifications for the program are described as a relation between the input and output variables expressed in predicate calculus. Mechanical theorem proving techniques are used to prove the existence of output variables satisfying the specifications. Existence is proven constructively, so that embedded in the proof is a method to compute the desired output values. A program is extracted from the proof. Restrictions to Robinson's resolution principle are proposed so that only constructive proofs are produced. A proof of the soundness of the method is presented. It is also shown that programs for the entire class of recursive functions may be written by automatic program writing. Thus nothing is lost by restricting application of the resolution principle. An implementation of the method which writes LISP programs is described. (Author)

Descriptors :   (*COMPUTER PROGRAMMING, ALGORITHMS), AUTOMATION, COMPUTER LOGIC, COMPILERS, ARTIFICIAL INTELLIGENCE, PROGRAMMING LANGUAGES, RECURSIVE FUNCTIONS, THESES

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE