Communications of the ACM

grammar specifies this set Exp2: Here the nonterminal T generates linear expressions, the nonterminal C generates tests used in conditionals, and for a test t and expressions e1 and e2, ITE(t, e1, e2) stands for if t then e1 else e2. Now f (x, y) = ITE((x ≤ y), y, x) satisfies the logical specification Spec1 and also belongs to the set Exp2. Observe that this expression does not involve addition of terms and thus can also be generated by the following simpler grammar that specifies the set Exp3 of expressions: Now suppose we change the logical requirement of the desired function f from Spec1 to Spec2: Observe that this is an under-specifi-cation since multiple functions can satisfy this logical constraint. If we choose the set of expressions to be Exp2, a possible solution is f (x, y) = ITE( (x ≤ y), y, x) + 1. However, this solution will no longer work if the set of expressions is Exp3. This ability to change the specification of the desired function by revising either the logical formula or the set of expressions offers a significant convenience in encoding synthesis problems.

Programming by examples. An appealing application of synthesis is to learn a program from representative input-to-output examples. The Flash-Fill feature in Microsoft Excel is a recent success of such a programming methodology in practice. 10, 11 It allows Excel users to perform string transformations using a small number of input-to-output examples. For example, consider the task of transforming names from one format to another as shown in Table 1. Formally, the semantic constraint on the desired function f from strings to strings is given by the formula with a conjunct for each of the rows, where the conjunct for the first row is of the form f (Nancy FreeHafer) = FreeHafer, N.

The set of string transformations supported by the domain specific language of Excel can be specified by the grammar below (simplified for exposition): In this grammar, the nonterminal E generates string transformations, and the nonterminal I generates inte-ger-valued index expressions. The Concat(s1, s2) function returns the concatenation of the strings s1 and s2, SubStr(s, i1, i2) returns the substring of the string s between the integer positions i1 and i2, Len(s) returns the length of the string s, and IndexOf (s1, s2, i) returns the index of the ith occurrence of the string s2 in the string s1.

A possible solution to the SyGuS problem is: Concat(s1, “,”, s2, “.”), where s1 is the expression SubStr(s, IndexOf(s, “ ”, 1) + 1, Len(s) ) and s2 is SubStr(s, 0, 1). This program concatenates the following four strings: the substring in the input string starting after the first whitespace; constant string “,”; the first character; and constant string “.”.

Program optimization. In automatic program optimization, we are given an original program f, and we want to find another program g such that the program g is functionally equivalent to f and satisfies specified syntactic constraints so it has better performance compared to f. The syntactic constraint can be used to rule out, or restrict, the use of certain operations deemed expensive.

As an example, consider the prob-
lem of computing the average of two
unsigned integer input numbers x
and y represented as bitvectors. The
obvious expression (x + y)/2 is not a
correct implementation since the
intermediate result (x + y) can cause
an overflow error. If the input num-
bers are bitvectors of length 32, an
alternative correct formulation can
first extend the given numbers to
64-bits to make sure that no overflow
error will be introduced when they are
summed up together, then divide by
2, and finally convert the result back
to 32-bits. This is specified by the
function:
where the operator bv64 converts a
32-bitvector to a 64-bitvector by con-
catenating 32 zeros to its left, and bv32
converts a 64-bitvector to a 32-bitvec-
tor by taking the 32 rightmost bits.

Since the result does not require more than 32-bits, we want to know if there exists an equivalent solution that works without using an extension to 64-bits. We can pose this as a SyGuS question: does there exist an expression that is equivalent to f (x, y) and is generated by the grammar: where + is addition, &, , ˆ are bitwise and, or, and xor,  and  are shift left and shift right, N is the set of integer constants between 0 and 31. Note that the grammar explicitly rules out the use of bitvector conversion operators bv64 and bv32 used in the original program f. A correct solution to the synthesis problem is the program

Template-based invariant synthesis. To verify that a program satisfies its correctness specification, one needs to identify loop invariants— conditions over program variables that are preserved by an execution of the loop. As a simple example consider the following program, where i, j, m, and n are integers: