一句话：提出 BeAFix，对有缺陷的 Alloy 规约进行有界穷举且可扩展的自动修复，并用断言剪枝。
声明式语言日益流行但难以调试，然而自动修复研究多集中于命令式程序，声明式语言修复工具稀缺。本文提出 BeAFix，面向基于一阶关系逻辑的声明式语言 Alloy，自动修复有缺陷的模型。其核心是一种有界穷举且可扩展的修复候选空间探索策略，并配合形式严谨的可靠剪枝，从而避免组合爆炸。与依赖单元测试的最先进 Alloy 修复方法不同，BeAFix 不需要测试，可直接利用形式声明式语言中常用的断言来定位与修复缺陷。作者用其他研究者收集的数千个真实故障模型进行评估，表明 BeAFix 能有效生成正确修复，并优于当前最先进方法。
The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite significant advances in the program repair of imperative languages, there is a dearth of repair techniques for declarative languages. This paper presents BeAFix, an automated repair technique for faulty models written in Alloy, a declarative language based on first-order relational logic. BeAFix is backed with a novel strategy for bounded exhaustive, yet scalable, exploration of the spaces of fix candidates and a formally rigorous, sound pruning of such spaces. Moreover, different from the state-of-the-art in Alloy automated repair, that relies on the availability of unit tests, BeAFix does not require tests and can work with assertions that are naturally used in formal declarative languages. Our experience with using BeAFix to repair thousands of real-world faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2103-00327,
title = {Bounded Exhaustive Search of Alloy Specification Repairs},
author = {Simon Gutierrez Brida and German Regis and Guolong Zheng and Hamid Bagheri and ThanhVu Nguyen and Nazareno Aguirre and Marcelo Frias},
booktitle = {ICSE},
year = {2021},
doi = {10.1109/icse43902.2021.00105}
}