paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Language-Parametric Reference Synthesis

语言参数化引用合成
OOPSLA 9(OOPSLA1)2025匹配度 2/10 · 论文属于语言参数化程序分析与重构(Statix/scope graphs 派生逆名称查找),与用户核心关注的 PL×LLM/Agent、浮点程序分析、贝叶斯程序分析均无直接交集;仅在静态分析与形式化规范层面有间接关联。引用 0 inbox
Daniel A. A. Pelsmaeker, Aron Zwaan, Casper Bach, Arjan J. Mooij
crossref: 2026-09-10

AI 速览

一句话:提出从 Statix 类型系统规范自动派生逆查找,并借助作用域图进行语言参数化的具体引用合成,以支持可靠重构。

现代 IDE 的自动重构需要保证名字绑定不变,但直接实现可靠的引用替换容易引入绑定错误或解析到错误声明。已有工作用 locked references 将绑定保持与变换分离,而合成具体引用需要语言名字查找函数的忠实逆函数,手动实现困难。本文提出从 Statix 元 DSL 书写的类型系统规范自动派生该逆函数,并利用作用域图(scope graphs)表示程序绑定结构,以推断限定引用的名称并恢复其语法结构。作者在 2528 个 Java、196 个 ChocoPy 和 49 个 Featherweight Generic Java 测试程序上为 locked references 合成具体引用,得到一种语言参数化的引用合成方法。

问题
自动重构需在变换后生成仍解析到原声明的具体引用,避免名字绑定错误;手工为每种语言编写名字查找逆函数困难且易错。
方法
从 Statix 类型系统规范自动派生逆查找函数,并基于 scope graphs 推断引用名称与语法结构来合成具体引用。
评估
在 2528 个 Java、196 个 ChocoPy 和 49 个 Featherweight Generic Java 测试程序上,为 locked references 合成具体引用,验证该语言参数化方法的有效性。
原文摘要(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 languageparametric method for synthesizing references.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3159,
  title = {Language-Parametric Reference Synthesis},
  author = {Daniel A. A. Pelsmaeker and Aron Zwaan and Casper Bach and Arjan J. Mooij},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA1},
  year = {2025},
  doi = {10.1145/3720481}
}