LLM 生成的 VeriFast 规范的实证研究

静态验证工具可以确保工业规模的软件，但需要大量的人力来编写规范。对于基于分离逻辑的静态验证器（SL 验证器）尤其如此，它们擅长验证堆操作程序，但需要许多复杂的辅助规范来推理堆结构。最近的工作应用 大语言模型 (LLM) 来生成代码、测试和证明，包括验证者的规范，但主要针对非 SL 验证者。为了弥补这一差距，本文全面评估了 LLM 在提示生成使用 SL 验证器 VeriFast 验证 303 C 函数的规范时的表现。我们分两个阶段探索了八种提示方法、十种 LLM 和三种输入类型。定量和定性分析用于评估 LLM 生成的代码和规范的功能行为、可验证性和错误。结果表明，LLM 保留了源代码和规范中的功能行为（均超过 91%），但取得了适度的验证成功（31.4%）。在我们的环境中，使用 Gemini 2.5 Pro 并提供正式合同可以提高成功率。此外，大多数错误（94%）来自 LLM 在 SL 验证器（例如 VeriFast）的领域特定知识方面的错误。这些发现为优化 LLM 生成的 SL 验证器规范提供了指导。