Doi: 10.1145/2076450.2076472

Software Synthesis Procedures

By Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter

abstract

Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succeed for a well-defined class of specifications. We propose to systematically generalize decision procedures into synthesis procedures, and use them to compile implicitly specified computations embedded inside functional and imperative programs. Synthesis procedures are predictable, because they are guaranteed to find code that satisfies the specification whenever such code exists. To illustrate our method, we derive synthesis procedures by extending quantifier elimination algorithms for integer arithmetic and set data structures. We then show that an implementation of such synthesis procedures can extend a compiler to support implicit value definitions and advanced pattern matching.

1. in TRoDuc Tion

Synthesis of software from specifications8, 15 promises to make programmers more productive. Despite substantial recent progress in techniques that generate short instruction sequences11 and program fragments, 21, 22 synthesis is limited to small pieces of code. We anticipate that this will continue to be the case for some time in the future, for two reasons: ( 1) synthesis is algorithmically a difficult problem, and ( 2) synthesis may require detailed specifications, which for large programs become difficult to write.

We expect that important practical applications of synthesis lie in its integration with compilers for general-purpose programming languages. To make this integration feasible, we aim to identify well-defined classes of expressions and synthesis algorithms guaranteed to succeed for these classes of expressions, just like a compilation attempt succeeds for any well-formed program. Our starting point for such synthesis algorithms are decision procedures.

A decision procedure for satisfiability of a class of
formulas accepts a formula (constraint) in its class, and
checks if for some values of its variables the formula evalu-
ates to true. On top of this basic functionality, many deci-
sion procedure implementations provide the additional
feature of generating a satisfying assignment (a model),
whenever the given formula is satisfiable. Such model-
generation functionality has many uses, including better
error reporting in verification and test-case generation.
An important insight is that the model generation facility
of decision procedures could also be used as an advanced
computation mechanism. Given a set of values for some
of the variables, a model-generating decision procedure
can at run-time find the values of the remaining variables
such that a given formula is true. Such a mechanism has
the potential to bring the algorithmic improvements of
decision procedures to declarative paradigms such as
Constraint Logic Programming, 10 which introduce search
as an intrinsic aspect of program execution. Instead of
changing the entire program execution platform to sup-
port search, we introduce a method to compile expressive
declarative constraints while retaining the existing execu-
tion and compilation technique for the remaining parts of
the program.