[1] The primary application of program synthesis is to relieve the programmer of the burden of writing correct, efficient code that satisfies a specification.
However, program synthesis also has applications to superoptimization and inference of loop invariants.
[2] During the Summer Institute of Symbolic Logic at Cornell University in 1957, Alonzo Church defined the problem to synthesize a circuit from mathematical requirements.
In the 1960s, a similar idea for an "automatic programmer" was explored by researchers in artificial intelligence.
[citation needed] Since then, various research communities considered the problem of program synthesis.
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.
[5] In 2013, a unified framework for program synthesis problems called Syntax-guided Synthesis (stylized SyGuS) was proposed by researchers at UPenn, UC Berkeley, and MIT.
[6] The input to a SyGuS algorithm consists of a logical specification along with a context-free grammar of expressions that constrains the syntax of valid solutions.
[7] For example, to synthesize a function f that returns the maximum of two integers, the logical specification might look like this: (f(x,y) = x ∨ f(x,y) = y) ∧ f(x,y) ≥ x ∧ f(x,y) ≥ y and the grammar might be: where "ite" stands for "if-then-else".
The expression would be a valid solution, because it conforms to the grammar and the specification.
[8] The competition used a standardized input format, SyGuS-IF, based on SMT-Lib 2.
For example, the following SyGuS-IF encodes the problem of synthesizing the maximum of two integers (as presented above): A compliant solver might return the following output: Counter-example guided inductive synthesis (CEGIS) is an effective approach to building sound program synthesizers.
CEGIS was inspired by counterexample-guided abstraction refinement (CEGAR).
[11] The framework of Manna and Waldinger, published in 1980,[12][13] starts from a user-given first-order specification formula.
For that formula, a proof is constructed, thereby also synthesizing a functional program from unifying substitutions.
The framework has been designed to enhance human readability of intermediate formulas: contrary to classical resolution, it does not require clausal normal form, but allows one to reason with formulas of arbitrary structure and containing any junctors ("non-clausal resolution").
Programs obtained by this approach are guaranteed to satisfy the specification formula started from; in this sense they are correct by construction.
[14] Only a minimalist, yet Turing-complete,[15] purely functional programming language, consisting of conditional, recursion, and arithmetic and other operators[note 3] is supported.
Case studies performed within this framework synthesized algorithms to compute e.g. division, remainder,[16] square root,[17] term unification,[18] answers to relational database queries[19] and several sorting algorithms.
After applying a transformation rule for the distributive law in line 11, the proof goal is a disjunction, and hence can be split into two cases, viz.
is valid (with respect to the original specification), while line 15 says "in case