Building operational semantics of programming languages as executable ontological models of programs

A critical factor in ensuring the quality of software written in current and next-generation programming languages is the ability to rely on a formal operational semantics of the language. This gives developers a systematic, well-founded way to address reliability, performance, and security in the target software. We introduce a new formal framework where operational semantics can be developed and used not as a traditional non-executable abstract system, but as runnable code. That brings several advantages: easier modification, the ability to run across different execution environments, testing and debugging, version control, and more. We illustrate our approach using a practically relevant subset of the widely used C programming language. The strengths of our semantics framework are demonstrated by comparing it against the most popular current approaches across a set of practically relevant criteria. The paper presents the Attribute-Based Modeling Language (ABML) — a new domain-specific language designed for ontological modeling of programs and for defining their operational semantics in executable form. We describe the proposed method for building executable operational semantics with ABML. A worked example shows how our approach applies to a practically relevant subset of C. We then build an enriched ontology of C by adding semantic attributes, define algorithms for computing those attributes in ABML, and discuss how the enriched ontology influences the development of operational semantics. A detailed review of related work lets us compare our approach to state-of-the-art frameworks in terms of meeting current requirements for operational semantics development.

programming languages, programming language ontology, ontological model of a programming language, operational semantics of a programming language

1. I. S. Anureev, “A Specification Language for Discrete Dynamic Systems Based on Ontologically Structured Knowledge,” System Informatics, no. 29, pp. 137–158, 2025, doi: 10.31144/si.2307-6410.2025.n29.p137-158.

2. C. Rhodes, “SBCL: A sanely-bootstrappable Common Lisp,” in Workshop on Self-sustaining Systems, 2008, pp. 74–86.

3. N. Chappe, L. Henrio, and Y. Zakowski, “Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR,” in Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025, pp. 283–298.

4. W. Steingartner and V. Novitzk'a, “Operational semantics in a domain-specific robot control language: A pedagogical use case,” Computer Science and Information Systems, vol. 21, no. 3, pp. 1077–1095, 2024.

5. S. Goncharov, S. Milius, L. Schr"oder, S. Tsampas, and H. Urbat, “Towards a higher-order mathematical operational semantics,” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, pp. 632–658, 2023.

6. E. Mahe, C. Gaston, and P. L. Gall, “Equivalence of denotational and operational semantics for interaction languages,” in International Symposium on Theoretical Aspects of Software Engineering, 2022, pp. 113–130.

7. G. Jouneaux, “Self-adaptable operational semantics,” phdthesis, Universit'e de Rennes, 2024. Available: https://theses.hal.science/tel-05136513/

8. J. Proencca and L. Edixhoven, “Caos: A reusable SCALA web animator of operational semantics,” in International Conference on Coordination Languages and Models, 2023, pp. 163–171.

9. Q. Chen et al., “The essence of Verilog: a tractable and tested operational semantics for Verilog,” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, pp. 234–263, 2023.

10. Z. Xu, H. Wang, and M. Sun, “Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs,” in International Symposium on Theoretical Aspects of Software Engineering, 2025, pp. 303–321.

11. S. Rechenberger and T. Frühwirth, “A Refined Operational Semantics for FreeCHR,” Electronic Proceedings in Theoretical Computer Science, vol. 439, pp. 278–293, 2026.

12. D. Lee, M. Cho, J. Kim, S. Moon, Y. Song, and C.-K. Hur, “Fair operational semantics,” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 811–834, 2023.

13. G. P. Leemrijse, T. T. P. Franken, and T. Neele, “Formalisation of a new weak Semantics for AuDaLa,” in Proceedings of the International Symposium on Automated Technology for Verification and Analysis, 2024, pp. 93–116.

14. P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing, “From sequential to multi-threaded Java: An event-based operational semantics,” in Proceedings of the Algebraic Methodology and Software Technology: 6th International Conference, 1997, pp. 75–90.

15. P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing, “An event-based structural operational semantics of multi-threaded Java,” in Formal syntax and semantics of Java, Springer, 1999, pp. 157–200.

16. S. Drossopoulou and S. Eisenbach, “Towards an operational semantics and proof of type soundness for Java.” 1998. Available: https://www.researchgate.net/profile/Sophia-Drossopoulou/publication/2274336_Towards_an_Operational_Semantics_and_Proof_of_Type_Soundness_for_Java/links/0deec53398518f1a48000000/Towards-an-Operational-Semantics-and-Proof-of-Type-Soundness-for-Java.pdf

17. E. Coscia and G. Reggio, “An operational semantics for Java.” 1998. Available: https://www.researchgate.net/profile/Eva-Coscia/publication/2292715_An_Operational_Semantics_for_Java/links/004635150d44744df9000000/An-Operational-Semantics-for-Java.pdf

18. S. O. Wesonga, “Javalite — An Operational Semantics for Modeling Java Programs,” mathesis, 2012.

19. N. Belblidia and M. Debbabi, “A Dynamic Operational Semantics for JVML,” Journal of Object Technology, vol. 6, no. 3, pp. 71–100, 2007.

20. I. Attali, D. Caromel, and S. O. Ehmety, “An Operational Semantics for the Eiffel Language,” INRIA, RR-2732, 1995.

21. I. Attali, D. Caromel, and M. Russo, “A formal executable semantics for Java,” in Proceedings of Formal Underpinnings of Java, an OOPSLA, 1998, pp. 1–13.

22. Y. Gurevich and J. K. Huggins, “The semantics of the C programming language,” in International Workshop on Computer Science Logic, 1992, pp. 274–308.

23. C. Wallace, “The semantics of the C++ programming language,” in Specification and validation methods, Oxford University Press, Inc., 1995, pp. 131–164.

24. J. Camilleri, “An operational semantics for OCCAM,” International Journal of Parallel Programming, vol. 18, pp. 365–400, 1989.

25. J. Matthews and R. B. Findler, “Operational semantics for multi-language programs,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 31, no. 3, pp. 1–44, 2009.

26. A. Verdejo and N. Marti-Oliet, “Executable structural operational semantics in Maude,” The Journal of Logic and Algebraic Programming, vol. 67, no. 1-2, pp. 226–293, 2006.

27. T. Str"oder, F. Emmes, P. Schneider-Kamp, J. Giesl, and C. Fuhs, “A linear operational semantics for termination and complexity analysis of ISO Prolog,” in International Symposium on Logic-Based Program Synthesis and Transformation, 2011, pp. 237–252.

28. G. Roșu and T. F. Șerbuanutua, “An overview of the K semantic framework,” The Journal of Logic and Algebraic Programming, vol. 79, no. 6, pp. 397–434, 2010.

29. T. Nipkow and G. Klein, Concrete semantics: with Isabelle/HOL. Springer, 2014.

30. V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhailov, and A. V. Promskii, “Towards verification of C programs. C-light language and its formal semantics,” Programming and Computer Software, vol. 28, pp. 314–323, 2002.

31. M. Norrish, “C formalised in HOL,” University of Cambridge, Computer Laboratory, UCAM-CL-TR-453, 1998.

32. P. Kelsen and Q. Ma, “A lightweight approach for defining the formal semantics of a modeling language,” in International Conference on Model Driven Engineering Languages and Systems, 2008, pp. 690–704.

33. G. J. Smeding, “An executable operational semantics for Python,” mathesis, Universiteit Utrecht, 2009. Available: http://gideon.smdng.nl/wp-content/uploads/thesis.pdf

34. M. A. K"ohl, “An executable structural operational formal semantics for Python.” 2021.

35. S. Foster, C.-K. Hur, and J. Woodcock, “Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL,” ACM Transactions on Software Engineering and Methodology, vol. 34, no. 4, pp. 1–40, 2025, doi: 10.1145/3702981.

36. F. Sheng, H. Zhu, J. He, Z. Yang, and J. P. Bowen, “Theoretical and Practical Aspects of Linking Operational and Algebraic Semantics for MDESL,” ACM Transactions on Software Engineering and Methodology, vol. 28, no. 3, pp. 1–46, 2019, doi: 10.1145/3295699.

37. Y. Huang, X. Bu, G. Zhu, X. Ye, X. Zhu, and J. Shi, “KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification,” IEEE Access, vol. 7, pp. 14593–14602, 2019, doi: 10.1109/ACCESS.2019.2894026.

38. D. Youn et al., “Bringing the WebAssembly Standard up to Speed with SpecTec,” vol. 8, no. PLDI, p. 210, 2024, doi: 10.1145/3656440.

39. D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, “Lem: reusable engineering of real-world semantics,” in Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, 2014, pp. 175–188. doi: 10.1145/2628136.2628143.