2026-06-01T09:55:32Zhttps://riuma.uma.es/rest/oai/request

oai:riuma.uma.es:10630/399492026-02-03T12:20:51Zcom_10630_2254col_10630_37959

Automatic Documentation of Java Code with Formal Specifications using Artificial Intelligence. Recio, Juan Carlos Saborido Infantes, Rubén Chicano-García, José-Francisco Métodos formales (Informática) Diseño de sistemas Proceso en lenguaje natural (Informática) Inteligencia artificial 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. 2025-09-17T08:14:29Z 2025-09-17T08:14:29Z 2025-09-17T08:14:29Z 2025-09 conference output https://hdl.handle.net/11705/JISBD/2025/90 https://hdl.handle.net/10630/39949 eng Jornadas de Ingeniería del Software y Bases de Datos (JISBD) Córdoba, España 9 a 11 de septiembre de 2025 http://creativecommons.org/licenses/by/4.0/ open access Atribución 4.0 Internacional