Interactive Code Generation

This thesis presents two approaches to code generation (synthesis) along with a discussion of other related and influential works, their ideas and relations to these approaches. The common goal of these approaches is to efficiently and effectively assist developers in software development by synthesizing code for them and save their efforts. The two presented approaches differ in the nature of the synthesis problem they try to solve. They are targeted to be useful in different scenarios, apply different set of techniques and can even be complementary. The first approach to code synthesis relies on typing information of a program to define and drive the synthesis process. The main requirement imposes that synthesized solutions have the desired type. This can aid developers in many scenarios of modern software development which typically involves composing functionality from existing libraries which expose a rich API. Our observation is that the developer usually does not know the right combination for composing API calls but knows the type of the desired expression. With the basis being the well-known type inhabitation problem we introduce a succinct representation for type judgements that significantly speed up the search for type inhabitants. Our method finds multiple solutions and ranks them before offering them to the developer. We implemented this approach as a plugin for the Eclipse IDE for Scala. From the evaluation we concluded that this approach goes beyond available related techniques and can be very useful in practical software development. In the second approach, synthesis of code is driven by explicit specification of code in terms of (formal) specification. The goal is to allow the developer to specify a program, by giving formal description of its behavior, rather than writing the code - the actual implementation is synthesized automatically. The practical value of such synthesis is immediately clear since this problem is generally hard. The approach solves this problem by combining existing tools for code generation, verification and testing within the synthesis process, and applies techniques for speeding it up. Interesting modifications to the synthesis driven by types were made to allow synthesizing expressions lazily, on demand, by searching for solutions in an incremental fashion. Results of the evaluation on several examples show that the implementation can be effective and useful in practice, while the approach still offers a lot of room for improvements.