用大模型自动生成高质量C++类不变式，提升代码可靠性。
ClassInvGen: Class Invariant Synthesis using Large Language Models
- 结合大模型生成类不变式与测试用例，协同优化规格质量。
- 在标准C++数据结构上生成的不变式正确率超纯大模型方法37%。
- 适用于高可信度真实代码，支持自动化验证与完整性评估。
以前提条件、后置条件和类不变式为代表的正式程序规范，有助于程序理解与动态/静态验证。然而，高质量规范的合成受限于表达能力或需采用声明式方式。现有工作已证明大模型可有效生成Python和Java的方法前/后条件，但未涉及类不变式。本文提出ClassInvGen，一种利用大模型生成可执行类不变式与测试输入的方法，针对主流语言C++。实验表明，ClassInvGen在生成质量上优于纯大模型方法及经典数据驱动工具Daikon。研究贡献包括一个标准C++数据结构基准集及测试框架，可用于通过测试与变异体衡量生成规范的正确性与完整性。此外，在广泛使用的高完整性C++代码库中进行了案例研究，验证了其实际应用价值。
原文摘要 · Abstract (English)
Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants. In this work, we describe ClassInvGen, a method for co-generating executable class invariants and test inputs to produce high-quality class invariants for a mainstream language such as C++, leveraging LLMs' ability to synthesize pure functions. We show that ClassInvGen outperforms a pure LLM-based technique to generate specifications (from code) as well as prior data-driven invariant inference techniques such as Daikon. We contribute a benchmark of standard C++ data structures along with a harness that can help measure both the correctness and completeness of generated specifications using tests and mutants. We also demonstrate its applicability to real-world code by performing a case study on several classes within a widely used and high-integrity C++ codebase.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。