2401.08807.md

背景

• 背景
  文章介绍了软件开发过程中形式化程序规范的重要性，它们在需求分析、软件测试和验证等多个阶段中扮演着关键角色。然而手动编写准确、全面的规范是极具挑战的，因此变得耗时且劳动强度大。现有的自动规范生成方法通常依赖预定义的模板或语法，无法准确描述复杂真实世界程序的行为和功能。

• 已有的工作 现有工作的方法在面对复杂程序时受限于预定义模板和语法规则的限制，生成的规格通常简化过度，不能准确捕捉到程序实际行为。

核心贡献

• 提出了一个名为 SpecGen 的新技术

  • 挑战1：如何准确地生成规范 SpecGen 利用大型语言模型（LLMs）的代码理解能力，以对话形式指导生成适当的规范。如果 LLM 未能生成正确规范，SpecGen 使用四种突变操作符对生成的规范进行修改，并通过一种新颖的启发式选择策略来选择可验证的规范。

  • 挑战2：提高规范的生成效率 SpecGen提出了一种基于突变的生成方法来提高规范的多样性，包括一组突变操作符和一种改进验证效率的新启发式选择策略。

实现与部署

实验结果表明 SpecGen 在 120 个测试用例中成功为 100 个程序生成了可验证的规范，超过了现有的纯 LLM 方法和传统规范生成工具如 Houdini 和 Daikon。对生成规范的质量进一步调查表明，SpecGen 能够全面地阐述输入程序的行为。此外，一个用户研究评估了生成规范的语义质量，证明了 SpecGen 能够准确且全面地描述程序行为。

总结

论文提出了 SpecGen，一个结合了大型语言模型和启发式选择策略的程序形式化规范自动生成技术。通过比较与现有工具和纯 LLM 方法，SpecGen 表现出更高效和准确的生成规范的能力，并且提出了数据集促进后续研究。