Deductive Programming Synthesis.

摘要

Program synthesis is the systematic derivation of a computer program to meet a given specification. The specification is a general description of the purpose of the desired program, while the program is a detailed description of a method for achieving that purpose. The method is based on a deductive approach, in which the problem of deriving a program is regarded as one of proving a mathematical theorem. The theorem expresses the existence of an object meeting the specified conditions. The proof is restricted to be sufficiently constructive to indicate a method for finding the desired output. That method becomes the basis for a program, which is extracted from the proof. The emphasis of the work has been on automating as much as possible of the program derivation process. Theorem-proving methods particularly well-suited to the program synthesis application have been developed. An interactive program-derivation system has been implemented. Applications to database management and planning have been investigated.