paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Constraint-Based Refactoring

基于约束的重构
TOPLAS 40(1)2018匹配度 3/10 · 论文属于程序重构与约束逻辑编程,关注工具正确性条件和实现算法,与用户核心方向(LLM/Agent 与静态分析/形式化验证交叉、浮点或贝叶斯程序分析)没有直接关联;仅在“理论形式化+工程实现”的 PL 工具研究偏好上有边缘参考价值。引用 15 inbox
Friedrich Steimann
crossref: 2026-09-10

AI 速览

一句话:将基于约束的重构从类型推广到名称、位置、可访问性等属性,并给出工具正确性条件与实现算法。

重构工具需要在对程序元素做变换时保持语义,但为多种重构和语言统一保证正确性并不容易。本文将 Tip 等人的基于约束的类型重构推广到名称、位置、可访问性等程序元素属性,先给出重构工具的通用规约,再把基于约束的重构发展为一类重构问题的通用方案,并给出使工具对任意目标语言都正确的条件。对于语义未形式化定义的语言,该条件可转化为自动化测试过程。作者提出基于约束逻辑编程的新算法,从待重构程序生成约束,并在开源程序上应用重构以评估时空开销。最后说明该框架可扩展到临时重构、跨语言重构以及模型与代码协同重构。

问题
如何以通用、可证明正确的方式支持类型之外的重构(名称、位置、可访问性等),并降低对目标语言形式语义的依赖。
方法
将基于约束的类型重构推广为约束驱动的重构框架,给出重构工具通用规约和正确性条件;提出基于约束逻辑编程的约束生成算法。
评估
在开源程序上实际应用重构,测量算法时间和空间需求;并说明正确性条件可用于自动化测试,框架可扩展至跨语言与模型/代码协同重构。
原文摘要(Abstract)

Constraint-based refactoring generalizes constraint-based type refactoring as introduced by Tip et al. [61] by extending the coverage of change from types to names, locations, accessibilities, and other properties of program elements. Starting with a generic specification of refactoring tools, we systematically develop constraint-based refactoring as a generic solution to a certain class of refactoring problems and provide a condition under which constraint-based refactoring tools are proven correct for any given target language. Although compliance with this correctness condition is hard to prove for target languages whose semantics is not formally defined, we show how the condition gives rise to automated testing procedures. We present a novel algorithm based on constraint-logic programming for the generation of constraints from a program to be refactored, and demonstrate its time and space requirements by using it in the application of refactorings to open source programs. Summarizing earlier work, we show how the principles underlying constraint-based refactoring tools extend to ad hoc refactoring, cross-language refactoring, and model/code co-refactoring.

链接与引用

DOI 原文 ·

BibTeX
@article{paperbot325,
  title = {Constraint-Based Refactoring},
  author = {Friedrich Steimann},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {40},
  number = {1},
  year = {2018},
  doi = {10.1145/3156016}
}