2026-05-29T20:39:54Zhttps://riuma.uma.es/rest/oai/request

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

00925njm 22002777a 4500 dc Recio, Juan Carlos author Saborido Infantes, Rubén author Chicano-García, José-Francisco author 2025-09 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. https://hdl.handle.net/11705/JISBD/2025/90 https://hdl.handle.net/10630/39949 Métodos formales (Informática) Diseño de sistemas Proceso en lenguaje natural (Informática) Inteligencia artificial Automatic Documentation of Java Code with Formal Specifications using Artificial Intelligence.