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

Application domain/field

Expected input

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.
Synthesis

Related papers

Program Sketching by Automatically Generating Mocks from Tests (CAV '21)

Last publication date

15 July 2021

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.