PV2 ⊧ Sketcham, short for Sketch and Mockssynthesises a full program from its sketch

Application domain/field

• Program synthesis
• Sketching
• Modular synthesis

Expected input

• Input sketch program

Format:

Sketch's intermediate representation

Expected output

Program sketch augmented with mock harnesses.

Internals

Sketch: Program written in a C-like language augmented with holes, unknown constants, and generators, unknown expressions. Harnesses: Way to specify the solution for a sketch using test cases that make assertions about the results. Mocks: Functions that, in place of full implementations, approximate the desired behavior with a specification in the form of assertions about individual cases. Sketcham converts a regular sketch problem into a modular sketch problem by automatically generating mocks from harnesses. Sketcham has been implemented as an additional pass to Sketch.