今天介绍的论文来自于南京大学、南洋理工大学、新加坡管理大学合作完成并投稿的，已被软件工程顶会ICSE 2025接收的论文SpecGen: Automated Generation of Formal Program Specifications via Large Language Models。

本文聚焦于形式化程序规约生成问题。程序规约主要是用来描述程序的语义与行为，它们在软件开发的多个环节中均可发挥重要作用。根据规约所采用的语言，程序规约可分为自然语言规约与形式化规约。其中，由于形式语言的无歧义性与可解析性，用形式语言写就的形式化程序规约对各项自动化软件工程技术具有难以替代的重要价值。然而，形式语言繁杂晦涩，人工阅读并手动编写完善的形式化程序规约难度较高，这促成了自动化程序规约生成技术的诞生。传统程序规约生成技术一般采用基于模版与规则的方法，只能覆盖有限的规约模式，泛用性不足，难以精准把握现实世界中程序的复杂行为和语义。

为了解决这一问题，作者创新性地将代码大模型引入程序规约生成任务中，以求利用其代码理解与总结能力生成更近于目标程序语义的程序规约。作者提出了一种全新的形式化程序规约生成技术，该技术分为两个阶段：对话驱动的规约生成，以及基于变异的规约生成。在第一阶段中，该技术采用与代码大模型进行对话的形式，利用精心设计的提示信息以及输入输出样例作为上下文，请求大模型生成目标程序的规约，并在对话中初步修复规约中的基础性错误。在第二阶段中，该技术采用启发式变异算法，用多种变异操作对上一阶段的结果进行变异，从而获得一系列候选规约，并采用启发式选择策略，从中筛选出一个可验证的规约子集作为最终结果，以求修复规约中的细节错误，增强规约的可验证性。

作者将以上形式化程序规约生成技术实现为原型工具SpecGen，用于为Java程序生成JML风格的程序规约，并将其与已有的传统规约生成方法以及基于大模型的规约生成方法进行比较。实验结果表明，在实验所涉及的385个Java程序中，SpecGen成功为279个程序生成了可验证的程序规约，远超传统规约生成方法，在基于大模型的规约生成方法中同样保持领先。同时，SpecGen表现出了接近60%的平均成功率，优于其他基于大模型的规约生成方法。进一步研究表明，技术所涉及的多种变异操作与启发式选择策略均可有效提升该技术的总体表现与效率。用户研究表明该技术所生成的规约强度接近于Ground Truth，能够有效反映目标程序的真实行为与语义。

1. 背景与动机

程序规约旨在描述程序的语义与行为。其中，“行为”既可以是软件设计意图上应当遵循的行为，也可以是程序实际运行过程中表现出的行为。代码中的注释、软件文档与手册、程序的正确性证明等都属于程序规约的范畴。程序规约在软件生命周期的多个环节内均能够发挥重要作用。例如，在需求分析环节，需求规约可以帮助软件开发者理清软件应当具备的功能细节；在软件开发环节，以注释为代表的规约能够提升代码可读性与易维护性；在软件测试环节，程序规约可以划清正确行为与异常行为的界限，从而帮助鉴别代码正确性。

程序规约具有不同的风格与语言。例如，代码注释与软件文档用自然语言写就，属于自然语言规约。区别于自然语言规约，由形式语言写就的形式化程序规约尤其具有非同小可的意义。形式语言经由严格的语法和语义定义而成，具有无歧义性与可解析性，前者使得它们具备清晰明确的语义，后者使得其语义可以由语法分析和语义分析算法解析获得。因而，形式化程序规约在各项自动化软件工程技术中具备广泛的应用前景。在规约语言方面，本文以JML（Java Modeling Language）为主要载体开展研究，这是一种针对Java程序的形式化建模语言，在程序规约语言中颇具代表性。下图展示了一个简单的Java程序以及相应的JML规约。该程序用于在整形数组nums中寻找两个元素，使它们的和恰好等于输入的整数target。描述该程序行为的规约主要可分为三个部分：第一个部分位于2~4行，其中requires语句描述函数twoSum的输入需要满足的约束，ensures语句描述函数twoSum的整体效果与功能；第二个部分位于7~9行，主要用maintaining语句描述外层循环的循环不变式；第三个部分位于11~13行，主要描述内层循环的循环不变式。

通过以上例子不难看出，形式化的程序规约一般采用类似数学表达式的建模语言，其内容往往非常繁杂晦涩，即使是非常简单的程序也可能需要大量形式化语句才能充分描述其行为。未经训练的软件开发者仅仅是阅读它们都可能非常吃力，人工为程序撰写形式化归约自然更加费时劳神。为了解决上述问题，自动化程序规约生成技术应运而生。传统的程序规约生成技术一般采用基于规则的方法，从一系列预先设置好的模版出发，在模板中填入目标程序内的变量名与操作符后，筛选出正确的模版并保留作为结果。这种做法的局限性显而易见：由于现实世界中软件的实际行为极其复杂，其规约往往也具有繁复多变的语法结构，而一套固定的预设模版只能覆盖非常有限的规约模式，这使得传统程序规约生成难以准确把握现实程序的行为与语义，面对复杂程序往往只能生成强度较低的简单规约，严重影响了其泛用性与应用前景。

大语言模型的兴起与盛行为这一困境带来了转机。现有的代码大模型经过了巨量代码数据集的训练，除了胜任一般的代码生成任务，它们还能够对代码进行一定程度上的理解与总结。从这一发现出发，本文力图将代码大模型融入程序规约生成技术中，利用其代码理解与总结能力，生成与目标程序语义更加接近的规约，从而解决传统程序规约生成技术泛用性不足的问题。

2. 技术方案

为了利用大语言模型解决上述难题，论文提出了一项全新的形式化程序规约生成技术。该技术分为两个阶段：

• 对话驱动的规约生成：该阶段通过与代码大模型进行对话的方式，向大模型请求生成目标程序的相关规约，并在对话中初步修复规约中的基础性错误；

• 基于变异的规约生成：该阶段以上一阶段的结果作为基础，通过启发式变异算法对大模型生成的规约进行变异与筛选，最终保留一系列可验证的规约作为最终结果。

2.1. 对话驱动的规约生成

为了将代码大模型的能力运用于规约生成任务中，作者采用了与模型进行对话的方式，以求在对话中尽可能充分利用代码大模型的上下文学习能力与代码理解能力。该阶段主要分为两个环节：初始提示构造以及对话式规约生成。首先，为了开启对话流程，作者利用少量样本学习（Few-shot Learning）技术构造对话初始上下文。初始上下文包括系统提示、数个输入输出样本范例以及真实初始请求三个部分。构造完成后，该上下文被作为初始提示信息提交给代码大模型，请求其为目标程序生成规约。通过提供样本范例，代码大模型得以对规约生成任务进行初步理解与认知，同时在这一过程中学习输出格式规范。

之后，代码大模型将根据以上提示生成初版程序规约。显然，模型的输出并不能保证完全正确。为了初步修复规约中的基础错误（包括语法错误等不符合JML规范的错误），作者利用已有的JML规约验证工具OpenJML对模型生成的规约展开验证。若验证通过，则这些规约将直接作为结果输出。否则，验证工具将返回一系列验证错误信息，作者将这些信息附于此前对话的上下文之后，并以此作为提示，继续请求大语言模型修复其中的错误。对于数种常见的基础错误，作者进一步提供了一系列预设的自然语言提示，将他们一并附于上下文之中，从而向模型提供可能的修复方案。基于以上信息，模型将继续尝试修复所生成规约中的错误，并生成新的规约。以上对话过程将持续迭代进行，直到模型所生成的规约成功通过验证工具的检查，或最大迭代次数被用尽。

2.2. 基于变异的规约生成

对于较简单的程序，对话驱动的规约生成能够较为轻松地驱使代码大模型生成合适的程序规约，并修复其中的基础性错误。然而，上述阶段仍不能保证修复规约中存在的一切错误。验证工具无法证明规约正确性的原因是复杂多样的，其反馈的错误信息也较为抽象晦涩，代码大模型时常无法透彻理解它们，难以分析错误背后的根因，进而无法对所生成规约进行有效修复。尽管如此，作者观察到，模型所生成的规约虽然可能无法通过验证，但其语法结构已经相当接近于正确规约，只是由于模型无法完美把握变量间的细节关系，其生成的规约在操作符等细节上容易出错，进而导致验证失败。从这一观察出发，作者提出了其技术的第二阶段，即基于变异的规约生成，用以修复规约中的细节错误，强化规约的可验证性。该阶段同样分为两个环节：模版规约变异与候选规约选择。

首先，作者将上一阶段中模型所生成的规约作为模版，对其进行启发式变异，以此得到一系列候选规约。根据JML语言所支持的操作符类型，作者设计了四种不同类型的变异操作，包括谓词变异、逻辑操作符变异、比较操作符变异以及算数操作符变异。每种变异操作均能将模版规约中的一处或多处相应类型操作符替换为同类型其他操作符。模版规约变异环节将穷举各种操作符的所有可能组合，从而得到所有可能的变种规约，并将它们视为候选规约。此后，候选规约选择环节将试图以迭代的方式从候选规约集合中筛选出一个可通过验证的规约子集。该环节首先将上一阶段模型所生成的所有规约视为当前所选择的规约集合，并尝试用规约验证工具对其加以验证。若验证未通过，验证工具将指出集合中的一条错误规约，并根据特定的启发式选择策略，从该规约所变异出的候选规约簇中选择一条规约，用其替代原错误规约，继续进行下一轮验证与选择迭代。该过程将持续迭代进行，直到所选择的规约集合成功通过验证，或所有候选规约均被验证工具否决。

3. 实验结果

作者将以上程序规约生成技术实现为原型工具SpecGen，将已有的传统规约生成技术和基于大模型的规约生成技术作为baseline进行比较。作者从SV-COMP数据集的Java类别中提取了265个Java程序作为benchmark，并额外手工收集了120个Java程序形成进一步的补充benchmark，以探究各方法在不同类别程序上的表现差异。实验结果表明：

• 在总计385个程序中，SpecGen为279个程序成功生成了可验证的程序规约，远超传统规约生成方法，领先于已有的基于大模型的规约生成方法；

• SpecGen表现出了接近于60%的平均成功率，在所有基于大模型的规约生成方法中保持领先；

• 基于大模型的规约生成方法表现普遍优于传统方法；

• 规约生成任务的难度与程序结构复杂性相关，含有循环的程序比不含循环的程序更难处理，含有嵌套循环的程序最具挑战性。

为了探究各方法在现实世界程序上的表现，作者进一步从知名数据集Defects4J中抽取了50个来自不同开源项目的Java程序。 实验结果表明，SpecGen成功处理了其中的38个程序，且能够维持55.20%的平均成功率，优于传统规约生成技术和基于对话式规约生成技术。

最后为了验证SpecGen所生成的规约是否能够有效反映目标程序语义，作者进一步展开了用户研究，选取15个不同方法均可处理的程序，邀请受试者对各方法所生成的规约有效性进行打分。结果表明，SpecGen所生成的程序规约强度接近于程序员手写的规约，显著领先于传统规约生成方法。更多的实验结果及分析，请参考原文。

4. 论文资源及项目开源