Details

Autor(en) / Beteiligte

• Leong, Iat Tou
• Barbosa, Raul

Titel

Translating meaning representations to behavioural interface specifications

Ist Teil von

• The Journal of systems and software, 2024-05, Vol.211, Article 112009

Ort / Verlag

Elsevier Inc

Erscheinungsjahr

2024

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• 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 Modelling Language. We evaluate the compiler on a set of representative benchmarks, including programs and specifications from the Java API, by generating Java Modelling Language specifications and statically checking them with a theorem prover. Results show that in 94% of the cases Java Modelling Language is accurately generated and in 97% of those cases it can be automatically checked with a state-of-the-art theorem prover. •Design of a compiler to translate higher-order logic meaning representations to JML.•Experimental evaluation of automated JML generation using a theorem prover.•A method to resolve ambiguities and provide semantic interpretation to meaning representations.•An approach to bridge the gap between Natural Language Processing and formal methods.