Incomputer science,program synthesis is the task to construct aprogram thatprovably satisfies a given high-levelformal specification. In contrast toprogram verification, the program is to be constructed rather than given; however, both fields make use offormal proof techniques, and both comprise approaches of different degrees of automation. In contrast toautomatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriatelogical calculus.^[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 tosuperoptimization and inference ofloop 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.^[3] 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.^{[citation needed]}

Since then, various research communities considered the problem of program synthesis. Notable works include the 1969 automata-theoretic approach byBüchi andLandweber,^[4] and the works byManna andWaldinger (c. 1980). The development of modernhigh-level programming languages can also be understood as a form of program synthesis.

This sectionneeds expansion with: a more detailed overview of contemporary approaches. You can help byadding missing information.(December 2022)

The early 21st century has seen a surge of practical interest in the idea of program synthesis in theformal verification community and related fields. Armando Solar-Lezama showed that it is possible to encode program synthesis problems inBoolean logic and use algorithms for theBoolean 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 atUPenn,UC Berkeley, andMIT.^[6] The input to a SyGuS algorithm consists of a logical specification along with acontext-free grammar of expressions that constrains the syntax of valid solutions.^[7] For example, to synthesize a functionf 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:

<Exp>::= x | y | 0 | 1 |<Exp> +<Exp> | ite(<Cond>,<Exp>,<Exp>)<Cond>::=<Exp> <=<Exp>

where "ite" stands for "if-then-else". The expression

ite(x <= y, y, x)

would be a valid solution, because it conforms to the grammar and the specification.

From 2014 through 2019, the yearly Syntax-Guided Synthesis Competition (or SyGuS-Comp) compared the different algorithms for program synthesis in a competitive event.^[8] The competition used a standardized input format, SyGuS-IF, based onSMT-Lib 2. For example, the following SyGuS-IF encodes the problem of synthesizing the maximum of two integers (as presented above):

(set-logic LIA)(synth-fun f ((x Int) (y Int)) Int  ((i Int) (c Int) (b Bool))  ((i Int (c x y (+ i i) (ite b i i)))   (c Int (0 1))   (b Bool ((<= i i)))))(declare-var x Int)(declare-var y Int)(constraint (>= (f x y) x))(constraint (>= (f x y) y))(constraint (or (= (f x y) x) (= (f x y) y)))(check-synth)

A compliant solver might return the following output:

((define-fun f ((x Int) (y Int)) Int (ite (<= x y) y x)))

Counter-example guided inductive synthesis (CEGIS) is an effective approach to building sound program synthesizers.^[9][10] CEGIS involves the interplay of two components: agenerator which generates candidate programs, and averifier which checks whether the candidates satisfy the specification.

Given a set of inputsI, a set of possible programsP, and a specificationS, the goal of program synthesis is to find a programp inP such that for all inputsi inI,S(p,i) holds. CEGIS is parameterized over a generator and a verifier:

• Thegenerator takes a set of inputsT, and outputs a candidate programc that is correct on all the inputs inT, that is, a candidate such that for all inputst inT,S(c,t) holds.
• Theverifier takes a candidate programc and returnstrue if the program satisfiesS on all inputs, and otherwise returns acounterexample, that is, an inpute inI such thatS(c,e) fails.

CEGIS runs the generator and verifier run in a loop, accumulating counter-examples:

algorithm cegisisinput: Program generatorgenerate,           verifierverify,           specificationspec,output: Program that satisfiesspec, or failureinputs := empty setloopcandidate :=generate(spec,inputs)ifverify(spec,candidate)thenreturncandidateelseverify yields a counterexamplee            adde toinputsend if

Implementations of CEGIS typically useSMT solvers as verifiers.

CEGIS was inspired bycounterexample-guided abstraction refinement (CEGAR).^[11]

Non-clausal resolution rules (unifying substitutions not shown)

Nr	Assertions	Goals	Program	Origin
51	${\displaystyle E[p]}$
52	${\displaystyle F[p]}$
53		${\displaystyle G[p]}$	s
54		${\displaystyle H[p]}$	t
55	${\displaystyle E[\text{true}]\vee F[\text{false}]}$			Resolve(51,52)
56		${\displaystyle \mathrm{\neg }F[\text{true}]\wedge G[\text{false}]}$	s	Resolve(52,53)
57		${\displaystyle \mathrm{\neg }F[\text{false}]\wedge G[\text{true}]}$	s	Resolve(53,52)
58		${\displaystyle G[\text{true}]\wedge H[\text{false}]}$	p? s: t	Resolve(53,54)

The framework ofManna andWaldinger, published in 1980,^[12][13] starts from a user-givenfirst-order specification formula. For that formula, a proof is constructed, thereby also synthesizing afunctional program fromunifying substitutions.

The framework is presented in a table layout, the columns containing:

• A line number ("Nr") for reference purposes
• Formulas that already have been established, including axioms and preconditions, ("Assertions")
• Formulas still to be proven, including postconditions, ("Goals"),^{[note 1]}
• Terms denoting a valid output value ("Program")^{[note 2]}
• A justification for the current line ("Origin")

Initially, background knowledge, pre-conditions, and post-conditions are entered into the table. After that, appropriate proof rules are applied manually. The framework has been designed to enhance human readability of intermediate formulas: contrary toclassical resolution, it does not requireclausal normal form, but allows one to reason with formulas of arbitrary structure and containing any junctors ("non-clausal resolution"). The proof is complete when${\displaystyle \mathit{t}\mathit{r}\mathit{u}\mathit{e}}$ has been derived in theGoals column, or, equivalently,${\displaystyle \mathit{f}\mathit{a}\mathit{l}\mathit{s}\mathit{e}}$ in theAssertions column. Programs obtained by this approach are guaranteed to satisfy the specification formula started from; in this sense they arecorrect by construction.^[14] Only a minimalist, yetTuring-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 torelational database queries^[19] and severalsorting algorithms.^[20][21]

Proof rules include:

• Non-clausalresolution (see table).

For example, line 55 is obtained by resolving Assertion formulas${\displaystyle E}$ from 51 and${\displaystyle F}$ from 52 which both share some common subformula${\displaystyle p}$. The resolvent is formed as the disjunction of${\displaystyle E}$, with${\displaystyle p}$ replaced by${\displaystyle \mathit{t}\mathit{r}\mathit{u}\mathit{e}}$, and${\displaystyle F}$, with${\displaystyle p}$ replaced by${\displaystyle \mathit{f}\mathit{a}\mathit{l}\mathit{s}\mathit{e}}$. This resolvent logically follows from the conjunction of${\displaystyle E}$ and${\displaystyle F}$. More generally,${\displaystyle E}$ and${\displaystyle F}$ need to have only two unifiable subformulas${\displaystyle p_1}$ and${\displaystyle p_2}$, respectively; their resolvent is then formed from${\displaystyle E\theta }$ and${\displaystyle F\theta }$ as before, where${\displaystyle \theta }$ is themost general unifier of${\displaystyle p_1}$ and${\displaystyle p_2}$. This rule generalizesresolution of clauses.^[22]

Program terms of parent formulas are combined as shown in line 58 to form the output of the resolvent. In the general case,${\displaystyle \theta }$ is applied to the latter also. Since the subformula${\displaystyle p}$ appears in the output, care must be taken to resolve only on subformulas corresponding tocomputable properties.

• Logical transformations.

For example,${\displaystyle E\wedge (F\vee G)}$ can be transformed to${\displaystyle (E\wedge F)\vee (E\wedge G)}$) in Assertions as well as in Goals, since both are equivalent.

• Splitting of conjunctive assertions and of disjunctive goals.

An example is shown in lines 11 to 13 of the toy example below.

• Structural induction.

This rule allows for synthesis ofrecursive functions. For a given pre- and postcondition "Given${\displaystyle x}$ such that${\displaystyle \mathit{\text{pre}}(x)}$, find${\displaystyle f(x)=y}$ such that${\displaystyle \mathit{\text{post}}(x,y)}$", and an appropriate user-givenwell-ordering${\displaystyle \prec }$ of the domain of${\displaystyle x}$, it is always sound to add an Assertion "${\displaystyle x^{\prime }\prec x\wedge \mathit{\text{pre}}(x^{\prime })⟹\mathit{\text{post}}(x^{\prime },f(x^{\prime }))}$".^[23] Resolving with this assertion can introduce a recursive call to${\displaystyle f}$ in the Program term.

An example is given in Manna, Waldinger (1980), p.108-111, where an algorithm to compute quotient and remainder of two given integers is synthesized, using the well-order${\displaystyle (n^{\prime },d^{\prime })\prec (n,d)}$ defined by (p.110).

Murray has shown these rules to becomplete forfirst-order logic.^[24]In 1986, Manna and Waldinger added generalized E-resolution andparamodulation rules to handle also equality;^[25] later, these rules turned out to be incomplete (but neverthelesssound).^[26]

Example synthesis of maximum function

Nr	Assertions	Goals	Program	Origin
1	${\displaystyle A=A}$			Axiom
2	${\displaystyle A\le A}$			Axiom
3	${\displaystyle A\le B\vee B\le A}$			Axiom
10		${\displaystyle x\le M\wedge y\le M\wedge (x=M\vee y=M)}$	M	Specification
11		${\displaystyle (x\le M\wedge y\le M\wedge x=M)\vee (x\le M\wedge y\le M\wedge y=M)}$	M	Distr(10)
12		${\displaystyle x\le M\wedge y\le M\wedge x=M}$	M	Split(11)
13		${\displaystyle x\le M\wedge y\le M\wedge y=M}$	M	Split(11)
14		${\displaystyle x\le x\wedge y\le x}$	x	Resolve(12,1)
15		${\displaystyle y\le x}$	x	Resolve(14,2)
16		${\displaystyle \mathrm{\neg }(x\le y)}$	x	Resolve(15,3)
17		${\displaystyle x\le y\wedge y\le y}$	y	Resolve(13,1)
18		${\displaystyle x\le y}$	y	Resolve(17,2)
19		${\displaystyle \mathit{\text{true}}}$	x<y? y: x	Resolve(18,16)

As a toy example, a functional program to compute the maximum${\displaystyle M}$ of two numbers${\displaystyle x}$ and${\displaystyle y}$ can be derived as follows.^{[citation needed]}

Starting from the requirement description "The maximum is larger than or equal to any given number, and is one of the given numbers", the first-order formula${\displaystyle \mathrm{\forall }X\mathrm{\forall }Y\mathrm{\exists }M:X\le M\wedge Y\le M\wedge (X=M\vee Y=M)}$ is obtained as its formal translation. This formula is to be proved. By reverseSkolemization,^{[note 4]} the specification in line 10 is obtained, an upper- and lower-case letter denoting a variable and aSkolem constant, respectively.

After applying a transformation rule for thedistributive law in line 11, the proof goal is a disjunction, and hence can be split into two cases, viz. lines 12 and 13.

Turning to the first case, resolving line 12 with the axiom in line 1 leads toinstantiation of the program variable${\displaystyle M}$ in line 14. Intuitively, the last conjunct of line 12 prescribes the value that${\displaystyle M}$ must take in this case. Formally, the non-clausal resolution rule shown in line 57 above is applied to lines 12 and 1, with

• p being the common instancex=x ofA=A andx=M, obtained by syntacticallyunifying the latter formulas,
• F[p] beingtrue ∧x=x, obtained frominstantiated line 1 (appropriately padded to make the contextF[⋅] aroundp visible), and
• G[p] beingx ≤ x ∧ y ≤ x ∧x = x, obtained from instantiated line 12,

yielding${\displaystyle \mathrm{\neg }(}$true ∧false) ∧ (x ≤ x ∧ y ≤ x ∧true${\displaystyle )}$,which simplifies to${\displaystyle x\le x\wedge y\le x}$.

In a similar way, line 14 yields line 15 and then line 16 by resolution. Also, the second case,${\displaystyle x\le M\wedge y\le M\wedge y=M}$ in line 13, is handled similarly, yielding eventually line 18.

In a last step, both cases (i.e. lines 16 and 18) are joined, using the resolution rule from line 58; to make that rule applicable, the preparatory step 15→16 was needed. Intuitively, line 18 could be read as "in case${\displaystyle x\le y}$, the output${\displaystyle y}$ is valid (with respect to the original specification), while line 15 says "in case${\displaystyle y\le x}$, the output${\displaystyle x}$ is valid; the step 15→16 established that both cases 16 and 18 are complementary.^{[note 5]} Since both line 16 and 18 comes with a program term, aconditional expression results in the program column. Since the goal formula${\displaystyle \mathit{\text{true}}}$ has been derived, the proof is done, and the program column of the "${\displaystyle \mathit{\text{true}}}$" line contains the program.

• Inductive programming
• Metaprogramming
• Program derivation
• Natural language programming
• Reactive synthesis
• Structural synthesis of programs

• David, Cristina; Kroening, Daniel (2017-10-13)."Program synthesis: challenges and opportunities".Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences.375 (2104) 20150403.Bibcode:2017RSPTA.37550403D.doi:10.1098/rsta.2015.0403.ISSN 1364-503X.PMC 5597726.PMID 28871052.
• Alur, Rajeev; Singh, Rishabh; Fisman, Dana; Solar-Lezama, Armando (2018-11-20). "Search-based program synthesis".Communications of the ACM.61 (12):84–93.doi:10.1145/3208071.ISSN 0001-0782.
• Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning in Program Synthesis".Artificial Intelligence.6 (2):175–208.doi:10.1016/0004-3702(75)90008-9.
• Solar-Lezama, Armando (2008).Program synthesis by sketching(PDF) (Ph.D.). University of California, Berkeley.

• Programming paradigms

• Harv and Sfn no-target errors
• Articles with short description
• Short description is different from Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from June 2010
• Articles to be expanded from December 2022
• All articles to be expanded
• Articles with unsourced statements from May 2016