Operational semantics of C jump statements in ABML

Operational semantics of C jump statements in ABML
Article's languageRussian
Abstract
- This paper presents an ontological approach to specifying the operational semantics of jump statements in the C programming language. The approach is based on ABML, a domain-specific language previously introduced for modeling discrete dynamic systems grounded in ontologically structured knowledge. We show that the operational semantics of programming language fragments, traditionally expressed as transition systems, can be viewed as dynamic systems and naturally formalized within the ABML framework. An ontology of C control-flow statements is introduced, covering goto, break, continue, and return, along with ontologies of constructs that respond to control transfer, including labeled statements, blocks, and the switch statement. The operational semantics of these ontological models is defined in terms of attribute closures computed with respect to agents and the execution environment. Particular attention is devoted to adapting ABML for the specification of operational semantics. This includes refining the concept of attribute closure, introducing explicit computation stages, and modeling the execution context explicitly. The resulting approach provides modularity, extensibility, and clarity in semantic specification. The results demonstrate the effectiveness of ontological modeling for the formal description of programming language semantics and establish a basis for extending the approach to additional C language constructs, as well as to program analysis and verification tasks.
DOI10.31144/si.2307-6410.2025.n29.p159-188
UDK004.451.2, 004.82, 004.021, 519.6, 004.42
Issue # 29,
Pages159-188
File anureev2025_2.pdf (403.79 KB)
Bibliographic reference
Anureev, I. Operational semantics of C jump statements in ABML. System Informatics 2025, 29, 159-188. https://doi.org/10.31144/si.2307-6410.2025.n29.p159-188.