000142733 001__ 142733
000142733 005__ 20190316234644.0
000142733 037__ $$aREP_WORK
000142733 245__ $$aOn Complete Functional Synthesis
000142733 269__ $$a2009
000142733 260__ $$c2009
000142733 336__ $$aReports
000142733 520__ $$aSynthesis 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 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 or give up a deterministic execution model.
000142733 6531_ $$asynthesis
000142733 6531_ $$adecision procedures
000142733 6531_ $$aprogramming language extensions
000142733 700__ $$aMayer, Mikaël
000142733 700__ $$0242187$$aSuter, Philippe$$g161402
000142733 700__ $$0242186$$aPiskac, Ruzica$$g179111
000142733 700__ $$0240031$$aKuncak, Viktor$$g177241
000142733 8564_ $$s261267$$uhttps://infoscience.epfl.ch/record/142733/files/main.pdf$$zn/a
000142733 909C0 $$0252019$$pLARA$$xU11739
000142733 909CO $$ooai:infoscience.tind.io:142733$$pIC$$preport$$qGLOBAL_SET
000142733 937__ $$aLARA-REPORT-2009-006
000142733 973__ $$aEPFL$$sPUBLISHED
000142733 980__ $$aREPORT