Automatic Documentation of Java Code with Formal Specifications using Artificial Intelligence

Abstract

We present a system that produces JML (Java Modeling Language) formal specifications of Java programming language code using Higher Order Logic (HOL). The system verifies that the formal specifications are correct using the Isabelle/HOL theorem prover assistant. Our approach combines automated unit test case generation, invariant detection, conversion between formal languages, and specialized Large Language Models (LLMs) for proof inference and formalized code documentation generation. This novel pipeline bridges the gap between practical software engineering and formal verification methods, enabling developers to automatically produce trustworthy documentation backed by mathematical proofs and formal statements that can later be combined in a modularized way to prove the correctness of large software systems.