Automatic Program Synthesis

该项目处理程序合成，即程序的派生以满足给定的规范。虽然规范描述了期望的程序要满足的条件，但程序本身描述了满足这些条件的详细方法。这项研究的好处是使编程过程更容易，更少受到错误的影响。该方法基于演绎法，将推导程序的问题视为证明数学定理的问题。该定理表示满足指定条件的对象的存在性。该证明仅限于具有足够的建设性，以指出一种寻找所需输出的方法。该方法成为从证明中提取的程序的基础。工作的重点是尽可能地使程序派生过程自动化。特别是，特别适合程序综合应用的定理证明方法已经开发出来。正在实施一个实验性的交互式程序派生系统。目前的研究课题包括开发一个更自动的定理证明器，修改已经构造的程序，以及控制派生程序的效率。

The project deals with program synthesis, the derivation of a program to meet a given specification. While the specification describes the conditions the desired program is to satisfy, the program itself describes a detailed method for meeting those conditions. The benefit of this research is to make the programming process easier and less subject to error. 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. In particular, theorem-proving methods particularly well-suited to the program synthesis application have been developed. An experimental interactive program-derivation system is being implemented. Current research topics included developing a more automatic theorem prover, modifying already constructed programs, and controlling the efficiency of derived programs.