-
Notifications
You must be signed in to change notification settings - Fork 3
InSynth future work
Some ideas that could potentially be used and refined for future work on InSynth. The list was compiled for the purpose of offering student semester projects at LARA. All ideas mentioned here are related to InSynth and may seem attractive later in case if InSynth becomes popular tool for Scala development within Scala IDE.
Note that the IDE (or more specifically Eclipse) part of some of these projects are optional and should not discourage students. In the contrary, Eclipse is a well designed platform (designed by smart software designers from multiple places and companies) and one can only learn basic, specialized things about Eclipse in order to be available to contribute to it.
It would be really helpful for developers if InSynth could provide some kind of descriptive information about resulting synthesized expressions. Since the main motivation for using InSynth is to aid the developer by synthesizing API calls so that the developer does not have to learn (huge) API (of many libraries and frameworks used in the project).
If InSynth generates an expression:
new SequenceInputStream(fileStream, System.in)
The developer might ask himself, why is that expression correct. If he had a quick and clean access to the API documentation relevant to declarations used in the synthesized expression he would be able to decide whether the expression is appropriate or not.
This may not be a trivial task, and of course there is a question how to present such results to the developer.
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- Java/Scala-doc framework
- Eclipse IDE (since the presentation of such results is important)
As usual, ideas on parallelizing a tool emerges. In this case it would greatly contribute to the practical value of InSynth.
It seems that InSynth has great potential for parallelization and it offers space for thinking about different parallelization strategies (parallelization of the engine searching, parallelization of the reconstruction phase, separation of the declaration extraction phase from the synthesis phase to make the whole process more efficient).
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- Scala concurrency framework
- (optional) Eclipse IDE concurrency framework
The idea is to allow the developer to input some additional parameters to synthesis, namely some expressions that should appear in the results of synthesis.
An example: The developer is sure that he should use his previously declared variable fileStream and the constructor of SequenceInputStream but is not sure how exactly. InSynth then can offer only expressions that satisfy his needs, e.g.:
new SequenceInputStream(fileStream, System.in)
This approach seems related to repairing type errors (and doing implicit conversion, in a limited number of steps) and can be used in some related scenarios.
This idea seems involving enough since the student should come up a way how to filter out expressions that satisfy the constraints. Also, on how to input these additional constraints.
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- (completely optional) Eclipse IDE (for inputing expressions)
Since the currently available option for checking correctness (type-check) of an expression at a specified placeholder is to plug the expression into the whole source code file and invoke the Scala compiler. Note that there is no way to insert just a Scala AST subtree at a given place in the tree and to invoke the compiler and thus avoid some unnecessary parts of the compilation process (as we got replies from the Scala team, this is currently not possible).
Student should figure out how to developed a system that could check correctness (perhaps something more than just a type-check) in a smarter way (without having to recompile the whole thing).
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- Scala compiler (AST, compilation process, phases...)
- (optional) Scala IDE
So far, InSynth works when invoked at a place of value (val, var, def) definition and also in some additional places such as if condition, and arguments (although the argument synthesis is somehow limited, due to problems of inferring the right argument type - which is basically the main idea of this project).
The idea is to extend the list of valid places where InSynth needs to be invoked by trying to infer types (that are then inputed to InSynth) at various other places (in case there is a possibility to do that). This requires getting familiar with Scala AST, type inference of the Scala compiler and seems as an interesting problem, especially for a student interested in theory of compilers (and modern compiler implementations).
This idea can (but may not) include interaction with an IDE, such that IDE helps the type inference by providing context information (e.g. Eclipse offers a list of completions, each completion can be an overloaded method call, thus can give information about parameters while they cannot be inferred easily).
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- Scala compiler (AST, compilation process, inference...)
- (optional) Scala IDE
This idea is motivated by the current problems we have with Scala version 2.10 and its build failing due to the changes that are continually being incorporated into newer versions of the Scala 2.10 (it seems that such changes are not being done in the case of Scala 2.9).
Goal would be to redesign the extraction loading phase of InSynth The extraction loading source code, includes a couple of files and the code there shows the things that one needs to care about when extracting information from Scala AST so the focus would be on designing a smart way for separating the loader that would not be so sensitive to changes made to Scala AST rather than on pure "playing with Scala AST".
One subgoal would be to make the loader more efficient since the declaration loading times dominate over rest of the total execution time of InSynth synthesis process (up to by two orders of magnitude). Separation of the loader phase and the synthesis phase (in terms of concurrency) could also bring improvements.
Note that this project could contribute not only to InSynth but also to Leon since Leon also has an extraction phase which depends on Scala AST (leon currently works only with Scala 2.9.1.).
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- Scala compiler (AST)
- (optional) concurrency
- (optional) Scala IDE
The idea of mutation testing with InSynth comes naturally to mind when one thinks about how to use InSynth for the purpose of software testing (together with some other, more involved ideas).
So the idea of mutation testing is clear and InSynth application seems natural, the rest of the work boils down to thinking how to implement it and perhaps how to provide it (within an IDE perhaps).
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- software testing
- (optional) Eclipse IDE
Having custom weights for each Scala file (or a project). The goal is to use different weights to achieve better results of synthesized snippets - after all, the weights that InSynth currently uses are hardcoded "magical" values.
This project would relate primarily to the InSynth weighting system (and the weights defined with no corpus). Student should come up with a smart implementation on how to change weights according to a:
- file being edited
- project in use
- project nature (e.g. web project)
- preferences of the developer
This project may touch questions related to the knowledge corpus - e.g. learning and upgrading current corpus based on choices of synthesized snippets given by the developer.
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- (optional) machine learning
- (optional) Eclipse IDE
The idea is to support writing of pattern matching code. Possible case statements could be examined and automatically given so that InSynth could get additional declarations for synthesis. A simple example would be, if the developer declared matching on expression e of type T
E match {
case ...
}
then InSynth could try expansion into case statements over all immediate subclasses of T and try to synthesize each case with newly introduced declarations.
This idea perhaps could be extended to support for comprehension. For example, if the developer needs a sequence (or a list) of values and some list declaration of some type already exists in the context, InSynth could offer for-comprehension over the existing list (note that this does not have to require polymorphism support in InSynth).
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem
- Scala compiler (AST)
- (optional) Eclipse IDE
This idea is motivated by many practical examples where solutions containing a certain call-chain or even an expression tree should be priotized.
For example: Available declarations are: x: Int, f1: Int → Boolean and f2: (Int, Int) → Boolean but for some reason the solution
f2(x, x)
should be prioritized over the solution
f1(x)
because, although it contains more declarations in its expression, the given combination is better (e.g. occurs more in practice).
Mentioned prioritizing of solutions can be enforced in the weighting system of InSynth but in which certain patterns, instead of just single declarations can be assigned specific weights. The phase that extracts solutions out of proof trees and relies on weights of declarations in this case should be changed and extended to allow reasoning on weights of subtrees (i.e. or patterns).
Student would have to think about a smart way on encoding weights of patterns and incorporating that into the synthesis process.
Related concepts:
- Getting familiar with InSynth synthesis algorithm and its approach to solving type inhabitation problem