Lune

CAV2021Top-tier venue

Program Sketching by Automatically Generating Mocks from Tests

Nate F. F. Bragg, Jeffrey S. Foster, Cody Roux, Armando Solar-Lezama

2021Year
4Citations

Abstract

Abstract Sketch is a popular program synthesis tool that solves for unknowns in a sketch or partial program. However, while Sketch is powerful, it does not directly support modular synthesis of dependencies, potentially limiting scalability. In this paper, we introduce Sketcham, a new technique that modularizes a regular sketch by automatically generating mocks—functions that approximate the behavior of complete implementations—from the sketch’s test suite. For example, if the function f originally calls g, Sketcham creates a mock gmg_m g m from g’s tests and augments the sketch with a version of f that calls gmg_m g m . This change allows the unknowns in f and g to be solved separately, enabling modular synthesis with no extra work from the Sketch user. We evaluated Sketcham on ten benchmarks, performing enough runs to show at a 95% confidence level that Sketcham improves median synthesis performance on six of our ten benchmarks by a factor of up to 5 ×\times × compared to plain Sketch, including one benchmark that times out on Sketch, while exhibiting similar performance on the remaining four. Our results show that Sketcham can achieve modular synthesis by automatically generating mocks from tests.

Ask about this paper

Your agent reads all of it.

Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.

Questions to start from

Your agent calls

Luneget_paper_fulltext

Ask in Lune

Free to start. No credit card required.

lune papers fulltext 02462ad5-11df-43ab-b6a3-bc3c3d678439

Builds on3

Related papers

Dusk over the sea between two cliffs drawn in fine vertical lines