SpecTune：以规格约束和中间行为信号改进程序修复

自动程序修复 (APR) 最近受益于 大语言模型 (LLM)。然而，大多数基于 LLM 的 APR 方法仍然主要依赖来自测试套件结果的粗粒度端到端信号或对候选修复程序的规范检查来指导修复，从而对程序内部逻辑偏离其预期行为的位置提供有限的洞察。相反，人工调试通常依赖于通过局部正确性条件或断言对程序状态进行中间推理。受这一观察的启发，我们提出了 SpecTune，这是一个规范引导的调试框架，它将中间行为推理纳入 APR 中。 SpecTune 将修复任务分解为由执行检查点连接的可疑区域，并派生代表这些点处的预期程序行为的局部后置条件。通过执行有缺陷的程序并评估这些后置条件，SpecTune 会生成微观级调试信号，指示观察到的行为与预期行为之间的不匹配，从而实现更精确的故障定位和有针对性的补丁生成。为了解决 LLM 生成的后置条件的潜在不可靠性问题，我们引入了两个互补信号：规范验证信号 alpha，它使用部分通过的测试用例估计生成的后置条件的一致性，以及判别信号 beta，它检测执行期间对已验证后置条件的违反。借助这些信号，SpecTune 可以安全地利用自动生成的 APR 规范。实验结果表明，SpecTune 比基线提高了故障定位和 APR 有效性。