Language-Parametric Reference Synthesis (Extended)
Daniel A. A. Pelsmaeker, Aron Zwaan, Casper Bach, Arjan J. Mooij
TL;DR
This paper tackles preserving name bindings during refactorings in languages with sophisticated binding rules by introducing language-parametric reference synthesis based on locked references. It derives a synthesizer for concrete references from declarative type specifications written in Statix, using scope graphs to guide the generation of valid, target-resolving references. The approach is evaluated on 2773 test programs across Java, ChocoPy, and FGJ, demonstrating soundness (synthetic references type-check and resolve to intended declarations) and substantial practical completeness, with most references synthesized within milliseconds to seconds. The work enables principled, language-parameterizable editor services and large-scale transformations by automating reference reconstruction, at the cost of higher computational effort in some complex cases. Data and artifacts are published to enable replication and further exploration of language-parametric reference synthesis.
Abstract
Modern Integrated Development Environments (IDEs) offer automated refactorings to aid programmers in developing and maintaining software. However, implementing sound automated refactorings is challenging, as refactorings may inadvertently introduce name-binding errors or cause references to resolve to incorrect declarations. To address these issues, previous work by Schäfer et al. proposed replacing concrete references with locked references to separate binding preservation from transformation. Locked references vacuously resolve to a specific declaration, and after transformation must be replaced with concrete references that also resolve to that declaration. Synthesizing these references requires a faithful inverse of the name lookup functions of the underlying language. Manually implementing such inverse lookup functions is challenging due to the complex name-binding features in modern programming languages. Instead, we propose to automatically derive this function from type system specifications written in the Statix meta-DSL. To guide the synthesis of qualified references we use scope graphs, which represent the binding structure of a program, to infer their names and discover their syntactic structure. We evaluate our approach by synthesizing concrete references for locked references in 2528 Java, 196 ChocoPy, and 49 Featherweight Generic Java test programs. Our approach yields a principled language-parametric method for synthesizing references.