Formal Methods Meets Readability: Auto-Documenting JML Java Code

TL;DR

This study shows that integrating JML formal specifications with LLM-generated Java documentation improves completeness and accuracy, especially for complex invariants, offering valuable insights for software documentation practices.

Contribution

It demonstrates that formal specifications like JML significantly enhance LLM-generated Java documentation quality, particularly for complex invariants and design contracts.

Findings

JML improves class-level documentation completeness

Formal specs help capture complex invariants

Benefits are more pronounced for classes with richer invariants

Abstract

This paper investigates whether formal specifications using Java Modeling Language (JML) can enhance the quality of Large Language Model (LLM)-generated Javadocs. While LLMs excel at producing documentation from code alone, we hypothesize that incorporating formally verified invariants yields more complete and accurate results. We present a systematic comparison of documentation generated from JML-annotated and non-annotated Java classes, evaluating quality through both automated metrics and expert analysis. Our findings demonstrate that JML significantly improves class-level documentation completeness, with more moderate gains at the method level. Formal specifications prove particularly effective in capturing complex class invariants and design contracts that are frequently overlooked in code-only documentation. A threshold effect emerges, where the benefits of JML become more pronounced for classes with richer sets of invariants. While JML enhances specification coverage, its impact on core descriptive quality is limited, suggesting that formal specifications primarily ensure comprehensive coverage rather than fundamentally altering implementation descriptions. These results offer actionable insights for software teams adopting formal methods in documentation workflows, highlighting scenarios where JML provides clear advantages. The study contributes to AI-assisted software documentation research by demonstrating how formal methods and LLMs can synergistically improve documentation quality.