ClassInvGen: Class Invariant Synthesis using Large Language Models
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911681222803456 |
|---|---|
| author | Sun, Chuyue Agashe, Viraj Chakraborty, Saikat Taneja, Jubi Barrett, Clark Dill, David Qiu, Xiaokang Lahiri, Shuvendu K. |
| author_facet | Sun, Chuyue Agashe, Viraj Chakraborty, Saikat Taneja, Jubi Barrett, Clark Dill, David Qiu, Xiaokang Lahiri, Shuvendu K. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_18917 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | ClassInvGen: Class Invariant Synthesis using Large Language Models Sun, Chuyue Agashe, Viraj Chakraborty, Saikat Taneja, Jubi Barrett, Clark Dill, David Qiu, Xiaokang Lahiri, Shuvendu K. Artificial Intelligence Programming Languages Software Engineering 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. |
| title | ClassInvGen: Class Invariant Synthesis using Large Language Models |
| topic | Artificial Intelligence Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2502.18917 |