Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction

Shihao Xia, Mengting He, Haomin Jia, Linhai Song

TL;DR

Doc2Spec tackles the challenge of generating formal programming specifications from natural-language programming rules by inducing a domain-specific grammar and guiding specification synthesis with a multi-agent framework. It localizes code entities, extracts attributes, identifies rules, induces a grammar in EBNF, and formalizes rules into a DSL-guided representation, validated by a parser checker. Across seven benchmarks in three languages, Doc2Spec achieves higher precision and recall than a non-grammar baseline and demonstrates practical utility by enabling bug detection in real-world smart contracts when integrated with a verification backend. The work highlights the effectiveness of automated grammar induction for improving reliability and quality in LLM-based specification generation, while outlining limitations and opportunities for richer logic, broader domains, and tighter verifier integration.

Abstract

Ensuring that API implementations and usage comply with natural language programming rules is critical for software correctness, security, and reliability. Formal verification can provide strong guarantees but requires precise specifications, which are difficult and costly to write manually. To address this challenge, we present Doc2Spec, a multi-agent framework that uses LLMs to automatically induce a specification grammar from natural-language rules and then generates formal specifications guided by the induced grammar. The grammar captures essential domain knowledge, constrains the specification space, and enforces consistent representations, thereby improving the reliability and quality of generated specifications. Evaluated on seven benchmarks across three programming languages, Doc2Spec outperforms a baseline without grammar induction and achieves competitive results against a technique with a manually crafted grammar, demonstrating the effectiveness of automated grammar induction for formalizing natural-language rules.

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction

TL;DR

Doc2Spec tackles the challenge of generating formal programming specifications from natural-language programming rules by inducing a domain-specific grammar and guiding specification synthesis with a multi-agent framework. It localizes code entities, extracts attributes, identifies rules, induces a grammar in EBNF, and formalizes rules into a DSL-guided representation, validated by a parser checker. Across seven benchmarks in three languages, Doc2Spec achieves higher precision and recall than a non-grammar baseline and demonstrates practical utility by enabling bug detection in real-world smart contracts when integrated with a verification backend. The work highlights the effectiveness of automated grammar induction for improving reliability and quality in LLM-based specification generation, while outlining limitations and opportunities for richer logic, broader domains, and tighter verifier integration.

Abstract

Ensuring that API implementations and usage comply with natural language programming rules is critical for software correctness, security, and reliability. Formal verification can provide strong guarantees but requires precise specifications, which are difficult and costly to write manually. To address this challenge, we present Doc2Spec, a multi-agent framework that uses LLMs to automatically induce a specification grammar from natural-language rules and then generates formal specifications guided by the induced grammar. The grammar captures essential domain knowledge, constrains the specification space, and enforces consistent representations, thereby improving the reliability and quality of generated specifications. Evaluated on seven benchmarks across three programming languages, Doc2Spec outperforms a baseline without grammar induction and achieves competitive results against a technique with a manually crafted grammar, demonstrating the effectiveness of automated grammar induction for formalizing natural-language rules.
Paper Structure (49 sections, 2 equations, 7 figures, 1 table)

This paper contains 49 sections, 2 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background and Related Work
  3. Natural Language API Rules
  4. Automated Formal Verification via LLMs
  5. Problem Formulation
  6. Design of Doc2Spec
  7. Stage 1: Localizing Programming Entities
  8. Stage 2: Extracting Entity Attributes
  9. Stage 3: Extracting Natural-Language Rules
  10. Stage 4: Inducing Rule Grammar
  11. Stage 5: Formalizing Rules
  12. Evaluation
  13. Experimental Setting
  14. Effectiveness and Comparison with Baselines
  15. Ablation Analysis
  16. ...and 34 more sections

Figures (7)

  • Figure 1: Comparison with existing solutions.
  • Figure 2: Textual description and a usage rule of a Rust standard library API. (The rule is highlighted in yellow.)
  • Figure 3: Textual description and an implementation rule of a public ERC20 API. (The rule is highlighted in yellow.)
  • Figure 4: Workflow of Doc2Spec. (LLM-based components are colored in blue, and Python program tools are colored in purple)
  • Figure 5: Simplified DSL Template.
  • ...and 2 more figures