首个带明确定义前提与后置条件的C++形式化规范数据集。
FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs
- 用大语言模型生成带预条件和后置条件的C++程序规范。
- 包含1000+个带有形式化规格的C++函数，支持验证工具评测。
- 适合研究程序验证、AI辅助开发及自动规范生成的开发者。
FormalSpecCpp 是一个旨在填补C++程序形式化规范验证标准基准空白的数据集。据我们所知，这是首个全面收录具有明确定义前提和后置条件的C++程序的综合性集合。该数据集为评估规范推断工具和测试生成规范的准确性提供了结构化基准。研究人员和开发者可利用该数据集对规范推断工具进行基准测试，微调大型语言模型（LLMs）以实现自动化规范生成，并分析形式化规范在提升程序验证与自动化测试中的作用。通过公开发布该数据集及代码，我们旨在推动程序验证、规范推断及人工智能辅助软件开发的研究进展。数据集与代码已开源：https://github.com/MadhuNimmo/FormalSpecCpp。
原文摘要 · Abstract (English)
FormalSpecCpp is a dataset designed to fill the gap in standardized benchmarks for verifying formal specifications in C++ programs. To the best of our knowledge, this is the first comprehensive collection of C++ programs with well-defined preconditions and postconditions. It provides a structured benchmark for evaluating specification inference tools and testing theaccuracy of generated specifications. Researchers and developers can use this dataset to benchmark specification inference tools,fine-tune Large Language Models (LLMs) for automated specification generation, and analyze the role of formal specifications in improving program verification and automated testing. By making this dataset publicly available, we aim to advance research in program verification, specification inference, and AI-assisted software development. The dataset and the code are available at https://github.com/MadhuNimmo/FormalSpecCpp.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。