Abstract Informal specifications of software artefacts need to be formalised to facilitate rigorous analysis, including deductive verification. Automated formalisation of informal specifications can significantly reduce the effort of manual translation. However, a major challenge lies in bridging the gap between the rich syntax of natural language and the need for precise semantics in formal specification languages. Building on the empirical observation that modern pre-trained large language models (LLMs) can effectively handle the breadth of natural language, while symbolic natural language processing (NLP) is more efficient in formal languages, this paper proposes an approach that combines both methodologies. The proposed solution, Hybrid Automated Formalisation of Informal Specifications (HAFIS), uses an LLM to restrict the syntax of informal specifications into the language of a formal grammar, and proposes the concept of Typed Semantic Interpretation to enforce the semantics of the resulting formal specifications. Using a public set of real-world informal specifications, we evaluated HAFIS and compared it with a purely symbolic approach and the direct use of LLMs as baselines. Results show that HAFIS increases language acceptance from 23% to 100% and accurately translates 88% of the cases into Java Modeling Language (JML). Furthermore, mutation analysis shows that the HAFIS-generated JML effectively finds defects in programs. These results substantiate that the proposed approach is effective and contributes to software analysis using natural language.

Higher-order logic can be used for meaning representation in natural language processing to encode the semantic relationships in text. Alternatively, using a formal specification language for meaning representation is more precise for specifying programs and widely supported by automatic theorem provers, while deductive verification based on higher order logic is less common for mainstream programming languages. This paper addresses the research question of translating higher-order logic meaning representations generated from method-level code comments into a formal specification language that extends first-order logic. Doing so requires resolving possible ambiguities in determining the appropriate semantics for predicates. This is an open challenge in the path toward using natural language processing with formal methods. To address this, the paper proposes an approach and constructs a compiler for translating meaning representations, generated from Java programs with method-level comments, into Java Modeling Language. We evaluate the compiler on a set of representative benchmarks, including programs and specifications from the Java API, by generating Java Modeling Language specifications and statically checking them with a theorem prover. Results show that in 94% of the cases Java Modeling Language is accurately generated and in 97% of those cases it can be automatically checked with a state-of-the-art theorem prover.