Complete Functional Synthesis

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. They should also support unbounded data types such as numbers and data structures. 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 extending decision procedures for integer linear arithmetic and data structures into synthesis procedures, and establishing results on the size and the efficiency of the synthesized code. We show that such procedures are useful as a language extension with...

• Type: Conference
• Year: 2010
• Where: PLDI
• Authors: Viktor Kuncak, Mika l Mayer, Ruzica Piskac, Philippe Suter
• Keywords: Complete Synthesis Procedures, Decision Procedures, PLDI 2010, Programming Languages, Synthesis Algorithms