Operational semantics of Rust expressions in ABML

The article provides a formal specification of the operational semantics of Rust expressions using the domain-specific modeling language ABML. It emphasizes the dynamic aspects of computation, including memory management, ownership, borrowing, and runtime verification of access conflicts. The approach relies on an ontological representation of Rust’s syntactic and semantic constructs, allowing expressions, blocks, and data structures to be described uniformly within a single computational model. Unlike traditional formalizations, this model explicitly integrates the safety metadata necessary to replicate Rust’s ownership and borrow checking mechanisms. A central contribution of this work is the use of a hierarchical memory model, which enables precise representation of partial borrows and access to individual fields within structures. This approach offers more accurate dynamic semantics than flat memory models and ensures consistency between formal rules and the actual behavior of Rust programs. The resulting operational semantics is executable and provides a foundation for program analysis, interpreter prototyping, and further research in the formal verification of languages with managed memory safety.