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