RT Conference Proceedings
T1 Automatic Documentation of Java Code with Formal Specifications using Artificial Intelligence.
A1 Recio, Juan Carlos
A1 Saborido Infantes, Rubén
A1 Chicano-García, José-Francisco
K1 Métodos formales (Informática)
K1 Diseño de sistemas
K1 Proceso en lenguaje natural (Informática)
K1 Inteligencia artificial
AB 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.
YR 2025
FD 2025-09
LK https://hdl.handle.net/10630/39949
UL https://hdl.handle.net/10630/39949
LA eng
NO Short paper submitted and accepted to the AI4SE track at JISBD 2025
NO Ministerio de Ciencia e Innovación (MICINN)
NO Ministerio de Ciencia, Innovación y Universidades
DS RIUMA. Repositorio Institucional de la Universidad de Málaga
RD 20 ene 2026