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 automation. In contrast to automatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriate logical calculus.

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.

Origin

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 1970s, 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.

Syntax-guided synthesis

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. 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. For example, to synthesize a function that returns the maximum of two integers, the logical specification might look like this:

and the grammar might be:

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. 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):

(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

Counter-example guided inductive synthesis (CEGIS) is an effective approach to building sound program synthesizers. CEGIS involves the interplay of two components: a generator which generates candidate programs, and a verifier which checks whether the candidates satisfy the specification.

Given a set of inputs , a set of possible programs , and a specification , the goal of program synthesis is to find a program in such that for all inputs in , (, ) holds. CEGIS is parameterized over a generator and a verifier:

• The generator takes a set of inputs , and outputs a candidate program that is correct on all the inputs in , that is, a candidate such that for all inputs in , (, ) holds.

• The verifier takes a candidate program and returns true if the program satisfies on all inputs, and otherwise returns a counterexample, that is, an input in such that (, ) fails.

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

algorithm cegis is
    input: Program generator generate,
           verifier verify,
           specification spec,
    output: Program that satisfies spec, or failure

    inputs := empty set
    loop
        candidate := generate(spec, inputs)
        if verify(spec, candidate) then
            return candidate
        else verify yields a counterexample e
            add e to inputs
        end if

Implementations of CEGIS typically use SMT solvers as verifiers.

CEGIS was inspired by counterexample-guided abstraction refinement (CEGAR).

The framework of Manna and Waldinger

The framework of Manna and Waldinger, published in 1980, 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 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"),

• Terms denoting a valid output value ("Program")

• 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 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 has been derived in the Goals in the Assertions column. Programs obtained by this approach are guaranteed to satisfy the specification formula started from; in this sense they are correct by construction. Only a minimalist, yet Turing-complete, purely functional programming language, consisting of conditional, recursion, and arithmetic and other operators is supported. Case studies performed within this framework synthesized algorithms to compute e.g. division, remainder, square root, term unification, answers to relational database queries and several sorting algorithms.

Proof rules

Proof rules include:

• Non-clausal resolution (see table).

• is the most general unifier. This rule generalizes resolution of clauses.

• appears in the output, care must be taken to resolve only on subformulas corresponding to computable properties.

• Logical transformations.

• ) 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 of recursive functions", and an appropriate user-given well-ordering". in the Program term.

• (p.110).

Murray has shown these rules to be complete for first-order logic. In 1986, Manna and Waldinger added generalized E-resolution and paramodulation rules to handle also equality; later, these rules turned out to be incomplete (but nevertheless sound).

Example

can be derived as follows.

Starting from the requirement description "The maximum is larger than or equal to any given number, and is one of the given numbers is obtained as its formal translation. This formula is to be proved. By reverse Skolemization, the specification in line 10 is obtained, an upper- and lower-case letter denoting a variable and a Skolem constant, respectively.

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. lines 12 and 13.

Turning to the first case, resolving line 12 with the axiom in line 1 leads to instantiation must take in this case. Formally, the non-clausal resolution rule shown in line 57 above is applied to lines 12 and 1, with

• being the common instance of and , obtained by syntactically unifying the latter formulas,

• being , obtained from instantiated line 1 (appropriately padded to make the context around visible), and

• being , obtained from instantiated line 12,

.

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 is valid; the step 1516 established that both cases 16 and 18 are complementary. Since both line 16 and 18 comes with a program term, a conditional expression" line contains the program.

See also

• Inductive programming

• Metaprogramming

• Program derivation

• Natural language programming

• Reactive synthesis

• Structural synthesis of programs

Notes

References