CONSTRUCTING PROGRAMS AUTOMATICALLY USING THEOREM PROVING

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 the...

Full description

Saved in:
Bibliographic Details
Main Author: Waldinger,Richard J
Format: Report
Language:English
Subjects:
ALGORITHMS
ARTIFICIAL INTELLIGENCE
AUTOMATIC COMPUTER PROGRAMMING
AUTOMATION
COMPILERS
COMPUTER LOGIC
COMPUTER PROGRAMMING
Computer Programming and Software
LISP PROGRAMMING LANGUAGE
PREDICATE CALCULUS
PROGRAMMING LANGUAGES
RECURSIVE FUNCTIONS
THESES
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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)