paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the Correctness of Software Merge

论软件合并的正确性
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 3/10 · 该论文研究软件合并的正确性准则与结构化合并工具,属于形式语义/软件工程方向;它不涉及 LLM/Agent、机器学习系统静态分析、浮点程序分析或贝叶斯程序分析,与用户当前核心研究问题仅有 PL/形式化方法的弱关联。引用 0 inbox
Akira Mori, Masatomo Hashimoto
crossref: 2026-09-12

AI 速览

一句话:提出可解析与universal的合并正确性准则,用范畴论pushout定义,并实现结构化合并工具揭示现有工具错误。

三方合并工具在现代开发中至关重要,但其正确性长期缺乏明确定义。本文提出语法正确性准则:合并结果须可解析(parsable),即符合源语言语法;且须普适(universal),即恰好包含各分支的编辑操作,公共编辑只应用一次。作者用范畴论中的pushout刻画universal条件,实现结构化合并工具,并与Git配套工具等比较。在76个开源Java项目、43,774个文件合并场景中,现有工具报告了若干错误结果,而该工具未报告错误。与2,582个开发者解决的合并及21类重构相关的2,459个场景对比,揭示了结构化合并的优势与局限,并强调明确正确性准则的重要性。

问题
三方合并工具被广泛使用,但其正确性缺乏明确、可检验的定义,工具输出常未受审查。
方法
提出parsable与universal两个语法准则,用范畴论pushout定义universal,并实现结构化合并工具进行对比。
评估
在76个开源Java项目的43,774个文件合并场景中实验,并与开发者解决合并及重构场景对比,发现现有工具存在错误而新工具无。
原文摘要(Abstract)

Three-way merge tools play crucial roles in modern software development, where a developer forks a branch to make local modifications and requests it to be merged into the main branch via a "pull request." Despite its importance, the task has traditionally been defined in an intuitive manner, and the results of merge tools are often accepted without scrutiny. In this paper, we present a new structural merge tool in comparison with existing tools based on the syntactic criteria we propose for evaluating the merge results. We require the merge result to be both parsable and universal. Being parsable means that the result is syntactically valid according to the grammar of the programming language. Being universal means that the result incorporates all and only the edit operations occurring in each branch while ensuring that edits common to both branches are applied only once. This requirement can be precisely defined using the notion of pushouts in category theory. In a large-scale experiment involving 43,774 file merge scenarios from 76 open-source Java projects, we found a number of incorrect results reported by existing tools such as the Git companion merge tool, whereas our tool reports none. We further compared d3j’s results with 2,582 developer-resolved merges and with 2,459 merge scenarios involving 21 refactoring types. These experiments revealed both the strengths and current limitations of structural merge, and underscore the importance of clear correctness criteria. We expect that the proposed criterion will provide a foundation for developing more reliable and principled merge tools.

链接与引用

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

BibTeX
@inproceedings{paperbot9411,
  title = {On the Correctness of Software Merge},
  author = {Akira Mori and Masatomo Hashimoto},
  booktitle = {ASE},
  year = {2025},
  doi = {10.1109/ase63991.2025.00193}
}