Mason: Type- and Name-Guided Program Synthesis

TL;DR

Mason presents a fragment-based approach to synthesizing object-oriented programs by guiding the search with typing constraints and naming information, enabling automatic insertion of design patterns into existing code. The core formalism defines a core OO language, constraint-based type inference, and synthesis rules, while the implementation in Scala demonstrates practical feasibility. Two extensions—trace-guided backtracking and name patterns—address search-space explosion and improve performance on larger benchmarks. Empirical evaluation across multiple design-pattern benchmarks shows Mason can solve many instances more efficiently with the extensions, marking a significant step toward automated multi-class OO program synthesis. The work lays groundwork for richer specifications and integration with lower-level or more expressive typing regimes.

Abstract

Object-oriented programs tend to be written using many common coding idioms, such as those captured by design patterns. While design patterns are useful, implementing them is often tedious and repetitive, requiring boilerplate code that distracts the programmer from more essential details. In this paper, we introduce Mason, a tool that synthesizes object-oriented programs from partial program pieces, and we apply it to automatically insert design patterns into programs. At the core of Mason is a novel technique we call type- and name-guided synthesis, in which an enumerative solver traverses a partial program to generate typing constraints; discharges constraints via program transformations guided by the names of constrained types and members; and backtracks when a constraint is violated or a candidate program fails unit tests. We also introduce two extensions to Mason: a non-local backtracking heuristic that uses execution traces, and a language of patterns that impose syntactic restrictions on missing names. We evaluate Mason on a suite of benchmarks to which Mason must add various well-known design patterns implemented as a library of program pieces. We find that Mason performs well when very few candidate programs satisfy its typing constraints and that our extensions can improve Mason's performance significantly when this is not the case. We believe that Mason takes an important step forward in synthesizing multi-class object-oriented programs using design patterns.

Figures (8)

• Figure 1: Partial Program Input to Mason
• Figure 2: Example Element of Fragment Library Provided to Mason. Holes begin with ? and are written in red.
• Figure 3: Mason's search for the correct Observer pattern implementation. Nodes denote synthesis steps and edges denote a particular choice taken at a given synthesis step. Each node is annotated with the candidate program before the synthesis step is taken and the interference or dependency sets of select steps are given in a box below. Leaves annotated with ✘ are candidates rejected for failing constraint resolution, or for failing unit tests. gray nodes and edges are paths left unexplored by trace-guided backtracking. The green dotted arrows trace the path of the search under trace-guidance.
• Figure 4: $\mathcal{L}_{M}$ Syntax, Types, and Constraints.
• Figure 5: Type Inference and Constraint Generation for $\mathcal{L}_{M}$.