合金规格修理的有界穷举搜索
Bounded Exhaustive Search of Alloy Specification Repairs
摘要：
声明性语言的日益普及及其难以调试的性质已经激发了对用于此类语言的适用的自动修复技术的需求。然而，尽管在命令式语言的程序修复方面取得了重大进展，但声明式语言的修复技术仍然缺乏。本文介绍了BeAFix，一种自动修复技术的错误模型写在合金，声明性语言的基础上一阶关系逻辑。BeAFix支持一种新颖的策略，用于对修复候选空间进行有界穷举但可扩展的探索，并对这些空间进行严格的合理修剪。此外，与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 realworld faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
