FormalSpecCpp

FormalSpecCpp是一个旨在填补C++程序形式化规范标准化基准空白的数据集。该数据集是首个包含良好定义的前置条件和后置条件的C++程序综合集。它为评估规范推导工具提供了一个结构化的基准，并可以用于调整大型语言模型以自动生成规范。该数据集由Dafny-synthesis基准转换而来，通过OpenAI的GPT-4-turbo模型系统地翻译成C++，确保生成的代码保持其形式化规范。该数据集可用于程序验证、规范推导和AI辅助软件开发等领域的研究。FormalSpecCpp is a dataset designed to fill the gap in standardized benchmarks for formal specifications of C++ programs. It is the first comprehensive collection of C++ programs with well-defined preconditions and postconditions. This dataset provides a structured benchmark for evaluating specification inference tools, and can be used to fine-tune large language models (LLMs) for automatic specification generation. Derived from the Dafny-synthesis benchmark, it was systematically translated into C++ using OpenAI's GPT-4-turbo model, ensuring that the generated code retains its formal specifications. This dataset can be applied to research in fields such as program verification, specification inference, and AI-assisted software development.

搜集汇总

数据集介绍

构建方式

FormalSpecCpp 数据集的构建方法是采用 Dafny-synthesis 作为基础，使用 OpenAI 的 GPT-4-turbo 模型通过提示驱动的翻译过程，将已验证的 Dafny 程序及其形式规格说明系统地转换为 C++ 程序，确保了形式和逻辑正确性的维持。这一过程涉及类型映射、断言转换和安全约束的明确处理，以减少错误并提高代码的语法正确性。

特点

FormalSpecCpp 数据集的特点在于它是首个全面的 C++ 程序集合，每个程序都定义了明确的先验条件和后验条件。该数据集为评估规格说明推断工具提供了一个结构化的基准，能够帮助研究人员和开发人员对推断工具进行基准测试，优化大型语言模型以自动生成规格说明，并分析形式规格在提高程序验证和自动化测试中的作用。

使用方法

使用 FormalSpecCpp 数据集的方法包括：作为规格说明推断工具的基准测试，用于微调大型语言模型以生成自动化规格说明，以及分析不同规格说明技术在软件正确性、工具性能和合同验证中的影响。数据集通过提供验证过的 C++ 程序和规格说明，支持静态和动态分析研究。

背景与挑战

背景概述

FormalSpecCpp数据集应运而生，旨在填补标准化的C++程序形式规范基准的空白。该数据集由加州大学河滨分校的Madhurima Chakraborty与劳伦斯利弗莫尔国家实验室的Peter Pirkelbauer和Qing Yi共同创建。FormalSpecCpp是首个全面的C++程序集合，其中包含了经过明确定义的先验条件和后验条件。它为评估规范推导工具提供了一个结构化的基准，并为自动化规范生成的大语言模型微调提供了可能。此数据集的公开可用，目的是推进程序验证、规范推导和AI辅助软件开发领域的研究。

当前挑战

FormalSpecCpp数据集在构建过程中遇到了诸多挑战。首先，由于C++缺乏对形式规范的原生支持，数据集的创建涉及到了将Dafny规格说明转换为C++的复杂过程。其次，Dafny与C++在类型系统和语言特性上的差异，使得翻译过程必须非常小心以避免引入错误。此外，自动化测试和手动验证翻译程序的正确性也是一个挑战，因为自动化方法可能无法捕捉到所有语义错误，而需要专家的人工审查。

常用场景

经典使用场景

FormalSpecCpp 数据集作为首个全面的 C++ 程序正式规范集合，其经典使用场景主要集中在为 C++ 程序的规范推断工具提供结构化的基准测试。该数据集通过将 Dafny 程序翻译成 C++，保留了其形式规范，使得研究人员和开发者可以在此基础上评估规范推断工具的精度、召回率和正确性，进而微调大型语言模型以自动化生成规范。

衍生相关工作

基于 FormalSpecCpp 数据集，研究者可以开展一系列相关工作，如进一步扩展数据集以包含更多程序和语言， refined 的提示工程过程，以及探索强化学习和混合方法来增强规范生成和验证的准确性。这些衍生工作有望推动程序验证和自动化程序分析领域的发展。

数据集最近研究

最新研究方向

FormalSpecCpp数据集为C++程序提供了标准化基准，以验证形式化规格。该数据集的创建旨在推进程序验证、规格推断以及AI辅助软件开发领域的研究。目前，该数据集在本领域的前沿研究方向主要集中在利用大型语言模型自动生成形式化规格，以及通过形式化规格改进程序验证和自动化测试。相关研究不仅关注规格推断工具的精确度、召回率和正确性评估，而且探讨不同规格技术对软件正确性、工具性能和合同验证的影响。FormalSpecCpp数据集的推出，为形式化规格在C++中的应用提供了实证基础，对提升软件可靠性具有重要意义。

相关研究论文

• FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs

  加州大学河滨分校, 劳伦斯利弗莫尔国家实验室 · 2025年