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:
String transformation by examples.
Input Output
Nancy FreeHafer FreeHafer, N.
Andrew Cencini Cencini, A.
Jan Kotas Kotas, J.