In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automatization. In contrast to automatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriate logical calculus.
During the Summer Institute of Symbolic Logic at Cornell University in 1957, Alonzo Church defined the problem to synthesize a circuit from mathematical requirements. Even though the work only refers to circuits and not programs, the work is considered to be one of the earliest descriptions of program synthesis and some researchers refer to program synthesis as “Church’s Problem”. In the 1960s, a similar idea for an “automatic programmer” was explored by researchers in artificial intelligence.
Since then, various research communities considered the problem of program synthesis. Notable works include the 1969 automata-theoretic approach by Büchi and Landweber, and the works by Manna and Waldinger (c. 1980). The development of modern high-level programming languages can also be understood as a form of program synthesis.
21st century developments
The early 21st century has seen a surge of practical interest in the idea of program synthesis in the formal verification community and related fields. Armando Solar-Lezama showed that it is possible to encode program synthesis problems in Boolean logic and use algorithms for the Boolean satisfiability problem to automatically find programs. In 2013, a unified framework for program synthesis problems was proposed by researchers at UPenn, UC Berkeley, and MIT. Since 2014 there has been a yearly program synthesis competition comparing the different algorithms for program synthesis in a competitive event, the Syntax-Guided Synthesis Competition or SyGuS-Comp. Still, the available algorithms are only able to synthesize small programs.
A 2015 paper demonstrated synthesis of PHP programs axiomatically proven to meet a given specification, for purposes such as checking a number for being prime or listing the factors of a number.
- ^Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). “Synthesis of programs in computational logic”. In M. Bruynooghe and K.-K. Lau (ed.). Program Development in Computational Logic. LNCS. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.
- ^Alonzo Church (1957). “Applications of recursive arithmetic to the problem of circuit synthesis”. Summaries of the Summer Institute of Symbolic Logic. 1: 3–50.
- ^Richard Büchi, Lawrence Landweber (Apr 1969). “Solving Sequential Conditions by Finite-State Strategies”. Transactions of the American Mathematical Society. 138: 295–311. doi:10.2307/1994916. JSTOR 1994916.
- ^Solar-Lezama, Armando (2008). Program synthesis by sketching (Ph.D.). University of California, Berkeley.
- ^Alur, Rajeev; al., et (2013). “Syntax-guided Synthesis”. Proceedings of Formal Methods in Computer-Aided Design. IEEE. p. 8.
- ^SyGuS-Comp (Syntax-Guided Synthesis Competition)
- ^Charles Volkstorf (7 Jan 2015). “Program Synthesis from Axiomatic Proof of Correctness”. arXiv:1501.01363 [cs.LO].
- ^Zohar Manna, Richard Waldinger (Jan 1980). “A Deductive Approach to Program Synthesis”. ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090.
- ^Zohar Manna and Richard Waldinger (Dec 1978). A Deductive Approach to Program Synthesis (PDF) (Technical Note). SRI International.
- ^See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.
- ^Manna, Waldinger (1980), p.108-111
- ^Zohar Manna and Richard Waldinger (Aug 1987). “The Origin of a Binary-Search Paradigm”. Science of Computer Programming. 9 (1): 37–83. doi:10.1016/0167-6423(87)90025-6.
- ^Daniele Nardi (1989). “Formal Synthesis of a Unification Algorithm by the Deductive-Tableau Method”. Journal of Logic Programming. 7: 1–43. doi:10.1016/0743-1066(89)90008-3.
- ^Daniele Nardi and Riccardo Rosati (1992). “Deductive Synthesis of Programs for Query Answering”. In Kung-Kiu Lau and Tim Clement (ed.). International Workshop on Logic Program Synthesis and Transformation (LOPSTR). Workshops in Computing. Springer. pp. 15–29. doi:10.1007/978-1-4471-3560-9_2.
- ^Jonathan Traugott (1986). “Deductive Synthesis of Sorting Programs”. Proceedings of the International Conference on Automated Deduction. LNCS. 230. Springer. pp. 641–660.
- ^Jonathan Traugott (Jun 1989). “Deductive Synthesis of Sorting Programs”. Journal of Symbolic Computation. 7 (6): 533–572. doi:10.1016/S0747-7171(89)80040-9.
- ^Manna, Waldinger (1980), p.99
- ^Manna, Waldinger (1980), p.104
- ^Manna, Waldinger (1980), p.103, referring to: Neil V. Murray (Feb 1979). A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. 2-79.
- ^Zohar Manna, Richard Waldinger (Jan 1986). “Special Relations in Automated Deduction”. Journal of the ACM. 33: 1–59. doi:10.1145/4904.4905.
- ^Zohar Manna, Richard Waldinger (1992). “The Special-Relations Rules are Incomplete”. Proc. CADE 11. LNCS. 607. Springer. pp. 492–506.