The growing adoption of declarative software specification languages, coupled with their inherent difficulty in debugging, has underscored the need for effective and automated repair techniques applicable to such languages. Researchers have recently explored various methods to automatically repair declarative software specifications, such as template-based repair, feedback-driven iterative repair, and bounded exhaustive approaches. The latest developments in large language models provide new opportunities for the automatic repair of declarative specifications. In this study, we assess the effectiveness of utilizing OpenAI's ChatGPT to repair software specifications written in the Alloy declarative language. Unlike imperative languages, specifications in Alloy are not executed but rather translated into logical formulas and evaluated using backend constraint solvers to identify specification instances and counterexamples to assertions. Our evaluation focuses on ChatGPT's ability to improve the correctness and completeness of Alloy declarative specifications through automatic repairs. We analyze the results produced by ChatGPT and compare them with those of leading automatic Alloy repair methods. Our study revealed that while ChatGPT falls short in comparison to existing techniques, it was able to successfully repair bugs that no other technique could address. Our analysis also identified errors in ChatGPT's generated repairs, including improper operator usage, type errors, higher-order logic misuse, and relational arity mismatches. Additionally, we observed instances of hallucinations in ChatGPT-generated repairs and inconsistency in its results. Our study provides valuable insights for software practitioners, researchers, and tool builders considering ChatGPT for declarative specification repairs.

翻译：声明式软件规约语言的日益普及，加上其本身调试的固有难度，凸显了对适用于此类语言的高效自动修复技术的需求。研究者近期探索了多种自动修复声明式软件规约的方法，例如基于模板的修复、反馈驱动的迭代修复和穷举有界修复。大语言模型的最新进展为声明式规约的自动修复提供了新的机遇。在本研究中，我们评估了利用OpenAI的ChatGPT修复以Alloy声明式语言编写的软件规约的有效性。与命令式语言不同，Alloy规约并非通过执行来评估，而是转化为逻辑公式，并利用后端约束求解器识别规约实例和断言的违反示例。本研究聚焦于ChatGPT通过自动修复提升Alloy声明式规约正确性与完备性的能力。我们分析了ChatGPT生成的结果，并与领先的Alloy自动修复方法进行了对比。研究表明，尽管ChatGPT在性能上逊于现有技术，但它能成功修复其他技术无法处理的缺陷。我们的分析还识别出ChatGPT生成修复中的错误，包括运算符使用不当、类型错误、高阶逻辑误用以及关系元数不匹配。此外，我们观察到ChatGPT生成的修复中存在幻觉现象及其结果的不一致性。本研究为考虑使用ChatGPT进行声明式规约修复的软件从业者、研究人员及工具开发者提供了宝贵见解。