Program synthesis
[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.[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".[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.[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.