טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentPeleg Hila
SubjectProgram Synthesis for Programmers
DepartmentDepartment of Computer Science
Supervisor Professor Eran Yahav
Full Thesis textFull thesis text - English Version


Abstract

Recent years have seen great progress in automated synthesis techniques that can automatically generate code based on some intent expressed by the user, but communicating this intent remains a major challenge. When the expressed intent is coarse-grained (for example, restriction on the expected type of an expression), the synthesizer often produces a long list of results for the user to choose from, shifting the heavy-lifting to the user. An alternative approach is programming by example (PBE), where the user leverages examples to interactively and iteratively refine the intent.

Existing program synthesis tools are usually designed around the synthesizer and its internals. However, these are tools intended for users, who are the ones who must specify (and respecify) the specifications. Synthesis tools are often designed either with no particular group of users in mind, or with the purpose of generating code for users who cannot write and read it.

This thesis focuses instead on designing synthesis tools specifically for programmers. This allows making assumptions on both the input the user can generate and the output they can consume. Concepts that are part of the programmer's life such as code review and unit tests can be leveraged.

We begin by discussing the human common sense of making generalizations can be aided by the user, as opposed to machine generalizations that rely on inductive bias. We draw from this the conclusion that some leaps of generalization or induction cannot be made by the synthesizer and are best left to a human. We demonstrate this on a non-iterative synthesizer JARVIS, which employs multiple biases but still required manual intervention by its user to improve the final result.

As a result of this, we set out to treat synthesis both as an iterative and an interactive process, involving the programmer in a gradual refinement of the specifications. But this approach also brings with it restrictions for the synthesizer, which pose new design challenges: examples, a common tool, are not expressive enough for programmers, who can observe the generated program and refine the intent by directly relating to parts of the generated program. Additionally, can the users correctly judge when the program is correct? We suggested a new Granular Interaction Model (GIM) and performed a controlled user study to assess its effectiveness.

In addition, we modeled the interaction of the user with a synthesizer, formalizing the refinement of specification by the user and the respective reduction of the candidate program space. This model allowed us to present two conditions for termination of a synthesis session, one hinging only on the properties of the available partial specifications, and the other also on the behavior of the user. Finally, we showed conditions for realizability of the user's intent, and limitations of backtracking when it is apparent a session will fail.