Functional Synthesis for Linear Arithmetic and Sets

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way---they should succeed for a well-defined class of specifications. To guarantee correctness and applicability to software (and not just hardware), these algorithms should also support unbounded data types, such as numbers and data structures. To obtain appropriate synthesis algorithms, we propose to generalize decision procedures into predictable and complete synthesis procedures. Such procedures are guaranteed to find code that satisfies the specification if such code exists. Moreover, we identify conditions under which synthesis will statically decide whether the solution is guaranteed to exist, and whether it is unique. We demonstrate our approach by starting from a quantifier elimination decision procedure for Boolean Algebra of set with Presburger Arithmetic (BAPA) and transforming it into a synthesis procedure. Our procedure also works in the presence of parametric coefficients. We establish results on the size and the efficiency of the synthesized code. We show that such procedures are useful as a language extension with implicit value definitions, and we show how to extend a compiler to support such definitions. Our constructs provide the benefits of synthesis to programmers, without requiring them to learn new concepts, give up a deterministic execution model, or provide code skeletons.

Citation

Viktor Kuncak, Mikael Mayer, Ruzica Piskac, and Philippe Suter. Functional synthesis for linear arithmetic and sets. Software Tools for Technology Transfer (STTT), TBD(TBD), 2012.

BibTex Entry

@article{KuncakETAL12FunctionalSynthesisLinearArithmeticSets,
  author = {Viktor Kuncak and Mikael Mayer and Ruzica Piskac and Philippe Suter},
  title = {Functional Synthesis for Linear Arithmetic and Sets},
  journal = {Software Tools for Technology Transfer (STTT)},
  year = 2012,
  abstract = {Synthesis of program fragments from specifications can make
programs easier to write and easier to reason about.  To
integrate synthesis into programming languages, synthesis
algorithms should behave in a predictable way---they should
succeed for a well-defined class of specifications. 
To guarantee correctness and applicability to software 
(and not just hardware), these algorithms
should also support unbounded data types, such as numbers and
data structures. 

To obtain appropriate synthesis algorithms, we propose to generalize decision
procedures into predictable and complete synthesis
procedures. Such procedures are guaranteed to find code that
satisfies the specification if such code exists. Moreover,
we identify conditions under which synthesis will statically
decide whether the solution is guaranteed to exist, and
whether it is unique.  We demonstrate our approach by
starting from a quantifier elimination decision procedure for Boolean Algebra
of set with Presburger Arithmetic (BAPA) and transforming it 
into a synthesis procedure. Our procedure also works in the presence
of parametric coefficients. We establish results on the size and the
efficiency of the synthesized code.  We show that such
procedures are useful as a language extension with implicit
value definitions, and we show how to extend a compiler to
support such definitions. Our constructs provide the
benefits of synthesis to programmers, without requiring them
to learn new concepts, give up a deterministic execution
model, or provide code skeletons.},
  volume = {TBD},
  number = {TBD}
}