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

https://doi.org/10.1007/978-3-030-81685-8_38 (CAV '21)

Last publication date

15 July 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.