JSketch

Sketch-based synthesis, epitomized by Sketch, lets developers synthesize software starting from a partial program, also called a sketch or template. JSketch is a tool that brings sketch-based synthesis to Java. JSketch's input is a partial Java program that may include holes, which are unknown constants, expression generators, which range over sets of expressions, and class generators, which are partial classes. JSketch then translates the synthesis problem into a Sketch problem; this translation is complex becuase Sketch is not object-oriented. Finally, JSketch synthesizes an executable Java program by interpreting the output of Sketch.

Publications

• JSketch: Sketching for Java. Jinseong Jeon, Xiaokang Qiu, Jeffrey S. Foster, and Armando Solar-Lezama. In 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE '15), Sep 2015.

Overview

The input to JSketch is an ordinary Java program that may also contain unknowns to be synthesized. There are two kinds of unknowns: holes, written ??, represent unknown integers and booleans, and generators, written {| e∗ |}, range over a list of expressions. For example, consider the following Java sketch, similar to an example from the Sketch manual:

class SimpleMath {
    static int mult2(int x) {
        return ?? * {| x , 0 |};
    }
}

Here we have provided a template for the implementation of method mult2: The method returns the product of a hole and either parameter x or 0. Notice that even this very simple sketch has 2^33 possible instantiations (32 bits of the hole and one bit for the choice of x or 0).

To specify the solution we would like to synthesize, we provide a harness containing assertions about the mult2 method:

class TestSimpleMath {
    harness static void test() {
        assert SimpleMath.mult2(3) == 6;
    }
}

Now we can run JSketch on the sketch and harness.

$ ./jsk.sh SimpleMath.java Test.java

The result is a valid Java source file in which holes and generators have been replaced with the appropriate code.

$ cat result/java/SimpleMath.java
class SimpleMath { ...
static public int mult2 (int x) {
return 2 * x;
} }

For more complex examples, view this project on github here and see regression test suites under test/ directory.

Limitations

As Java is a very large language, this tool currently only supports a core subset of Java. Unsupported features include: packages, access control, exceptions, and concurrency.

Additionally, JSketch assumes the input sketch is type correct, meaning the standard parts of the program are type correct, holes are used either as integers or booleans, and expression generators are type correct.