Manna and Waldinger 1971(ID:8180/)
Deductive automatic programming system. Development of PROW and forerunner of TABLOG
Related languages
References:
Manna, Zohar; Waldinger, Richard J. "Toward automatic program synthesis", Communications of the ACM, v.14 n.3, p.151-165, March 1971 view details
Leavenworth, Burt M.; Sammet, Jean E. "An overview of nonprocedural languages" pp1-12 view details
Abstract: This paper attempts to describe some of the basic characteristics and issues involving the class of programming languages commonly referred to as ?nonprocedural? or ?very high level?. The paper discusses major issues such as terminology, relativeness, and arbitrary sequencing. Five features of nonprocedural languages are described, and a number of specific languages are discussed briefly. A short history of the subject is included.
Extract: Manna and Waldinger system
Another system, called PROW {Waldinger and Lee, ]969), generates programs from descriptions of their inputs and outputs in the predicate calculus and also uses a resolution theorem prover. A similar use of the predicate calculus as a programming language, but not using an automatic theorem prover, is illustrated by Manna and Waldinger (1971).
in Proceedings of the ACM SIGPLAN symposium on Very high level languages, March 28-29, 1974, Santa Monica, California, United States view details
Manna, Zohar and Waldinger, Richard "Synthesis: dreams of programs", iEEE Trans. Sofiw. Eng. SE-5, 4 (July 1979), 294-328. view details
in Proceedings of the ACM SIGPLAN symposium on Very high level languages, March 28-29, 1974, Santa Monica, California, United States view details
Manna, Zohar and Waldinger, Richard "A Deductive Approach to Program Synthesis" ACM Transactions on Programming Languages and Systems (TOPLAS) vol2(1) January 1980 pp 90-121 1980 view details
Abstract: Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework.
External link: Online copy
in Proceedings of the ACM SIGPLAN symposium on Very high level languages, March 28-29, 1974, Santa Monica, California, United States view details
|