DEDALUS - The DEDuctive ALgorithm Ur-Synthesizer
DEDALUS - The DEDuctive ALgorithm Ur-Synthesizer
复制标题
DEDALUS - 演绎算法原始合成器
DOI：
10.1109/afips.1978.66
复制
发表时间：
1899
影响因子：
4.4
通讯作者：
R. Waldinger
中科院分区：
文献类型：
--
作者：
Z. Manna;R. Waldinger
程序综合是自动构造程序以满足给定的规范。这些规范构成了对所需程序的高级描述，它表达了程序的目的，但没有指明实现该目的的方法。这些规范用许多结构来表达，这些结构是所需程序的特定主题领域所特有的（例如，数字、集合、列表）。因为这些构造只用于描述程序的目的，不需要计算，所以它们可以比任何编程的构造都高得多。语言（例如，它们可以包括逻辑量词、集合构造器和其他不可计算的操作）。规格说明语言可以与程序员在思考问题时实际使用的概念紧密对应。我们正在开发的技术与目标编程语言的选择无关。我们在示例和实验系统中使用的特定语言是一种简单的类LISP语言，只包含基本的数值和列表处理操作、条件表达式和递归。在考虑程序的形成与副作用，我们扩展了语言，包括分配给变量，数组元素，和其他数据结构组件。我们的基本方法是根据一定的规则反复转换规范;每个规则用另一个等价的段替换程序描述的一个段。这个过程一直持续到获得一个完全根据目标语言的基本结构的描述;这个描述就是所需的程序。
Program synthesis is the automatic construction of programs to meet given specifications. These specifications constitute a high-level description of the desired program which expresses the purpose of the program, without indicating the method by which that purpose is to be achieved. The specifications are expressed in terms of many constructs which are endemic to the particular subject domain of the desired program (e.g., numbers, sets, lists). Because these constructs are only intended to describe the purpose of the program and need not be computed, they can be of a much higher level than the constructs of any programming . language (e.g., they can include logical quantifiers, set constructors, and other noncomputable operations). The specification language can correspond closely with the concepts a programmer actually uses in thinking about the problem. The techniques we are developing are independent of the choice of a target programming language. The particular language we use in our examples and in our experimental system is a simple LISP-like language containing only basic numerical and list-processing operations, conditional expressions, and recursion. In considering the formation of programs with side effects, we extend the language to include assignments to variables, array elements, and other data-structure components. Our basic approach is to transform the specifications repeatedly according to certain rules; each rule replaces one segment of a program description by another, equivalent, segment. The process continues until a description is obtained that is entirely in terms of the primitive constructs of the target language; this description is the desired program.