maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2026-2-122-149mais-2090Research ArticleTheory of SoftwareПостроение операционной семантики языков программирования в виде исполняемых онтологических моделей программBuilding operational semantics of programming languages as executable ontological models of programshttps://orcid.org/0000-0001-9574-128XАнуреевИгорь СергеевичAnureevIgor S.anureev@gmail.comhttps://orcid.org/0000-0001-9734-3808ГаранинаНаталья ОлеговнаGaraninaNatalia O.garanina@iis.nsk.suhttps://orcid.org/0000-0002-9387-6735КондратьевДмитрий АлександровичKondratyevDmitry A.apple-66@mail.ruhttps://orcid.org/0000-0003-3857-9380ГорлачСергей ПетровичGorlatchSergei P.gorlatch@uni-muenster.deИнститут систем информатики им. А.П. Ершова СО РАНРоссияA.P. Ershov Institute of Informatics Systems SB RASRussian FederationМюнстерский университетРоссияUniversity of MuensterRussian Federation202618062026332122149Copyright © Ануреев И.С., Гаранина Н.О., Кондратьев Д.А., Горлач С.П., 20262026Ануреев И.С., Гаранина Н.О., Кондратьев Д.А., Горлач С.П.Anureev I.S., Garanina N.O., Kondratyev D.A., Gorlatch S.P.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/2090

Важнейший аспект обеспечения качества программ, написанных на существующих и перспективных языках программирования, — это возможность опираться на формальную операционную семантику языка. Такой подход позволяет разработчикам системно и обоснованно решать вопросы надёжности, производительности и безопасности целевого программного обеспечения. Мы предлагаем новую формальную среду, в которой операционную семантику можно разрабатывать и использовать не как традиционную невыполнимую абстрактную систему, а как исполняемый программный код. Это даёт множество преимуществ: упрощение модификации, возможность выполнения в разных средах исполнения, тестирование и отладку, управление версиями и так далее. Мы иллюстрируем наш подход на примере практически значимого фрагмента широко используемого языка программирования C. Преимущества нашей среды для построения семантики демонстрируются путем сравнения с наиболее популярными современными подходами по набору практически значимых требований. В работе представлен язык моделирования на основе атрибутов (ABML) — новый предметно-ориентированный язык, предназначенный для онтологического моделирования программ и определения их операционной семантики в исполняемой форме. Описан предлагаемый подход к построению выполняемой операционной семантики с использованием ABML. Мы приводим также модельный пример, демонстрирующий применение нашего подхода к практически значимому фрагменту широко используемого языка программирования C. Далее строится обогащённая онтология языка C путём добавления семантических атрибутов, задаются алгоритмы вычисления этих атрибутов в ABML и обсуждается, как обогащённая онтология влияет на разработку операционной семантики. Подробный обзор связанных работ позволяет сравнить предлагаемый подход с современными фреймворками с точки зрения соответствия актуальным требованиям к разработке операционной семантики.

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 languagesprogramming language ontologyontological model of a programming languageoperational semantics of a programming languageReferencesI. 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.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.C. Rhodes, “SBCL: A sanely-bootstrappable Common Lisp,” in Workshop on Self-sustaining Systems, 2008, pp. 74–86.C. Rhodes, “SBCL: A sanely-bootstrappable Common Lisp,” in Workshop on Self-sustaining Systems, 2008, pp. 74–86.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.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.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.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.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.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.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.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.G. Jouneaux, “Self-adaptable operational semantics,” phdthesis, Universit'e de Rennes, 2024. Available: https://theses.hal.science/tel-05136513/G. Jouneaux, “Self-adaptable operational semantics,” phdthesis, Universit'e de Rennes, 2024. Available: https://theses.hal.science/tel-05136513/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.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.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.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.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.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.S. Rechenberger and T. Frühwirth, “A Refined Operational Semantics for FreeCHR,” Electronic Proceedings in Theoretical Computer Science, vol. 439, pp. 278–293, 2026.S. Rechenberger and T. Frühwirth, “A Refined Operational Semantics for FreeCHR,” Electronic Proceedings in Theoretical Computer Science, vol. 439, pp. 278–293, 2026.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.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.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.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.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.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.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.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.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.pdfS. 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.pdfE. 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.pdfE. 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.pdfS. O. Wesonga, “Javalite — An Operational Semantics for Modeling Java Programs,” mathesis, 2012.S. O. Wesonga, “Javalite — An Operational Semantics for Modeling Java Programs,” mathesis, 2012.N. Belblidia and M. Debbabi, “A Dynamic Operational Semantics for JVML,” Journal of Object Technology, vol. 6, no. 3, pp. 71–100, 2007.N. Belblidia and M. Debbabi, “A Dynamic Operational Semantics for JVML,” Journal of Object Technology, vol. 6, no. 3, pp. 71–100, 2007.I. Attali, D. Caromel, and S. O. Ehmety, “An Operational Semantics for the Eiffel Language,” INRIA, RR-2732, 1995.I. Attali, D. Caromel, and S. O. Ehmety, “An Operational Semantics for the Eiffel Language,” INRIA, RR-2732, 1995.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.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.Y. Gurevich and J. K. Huggins, “The semantics of the C programming language,” in International Workshop on Computer Science Logic, 1992, pp. 274–308.Y. Gurevich and J. K. Huggins, “The semantics of the C programming language,” in International Workshop on Computer Science Logic, 1992, pp. 274–308.C. Wallace, “The semantics of the C++ programming language,” in Specification and validation methods, Oxford University Press, Inc., 1995, pp. 131–164.C. Wallace, “The semantics of the C++ programming language,” in Specification and validation methods, Oxford University Press, Inc., 1995, pp. 131–164.J. Camilleri, “An operational semantics for OCCAM,” International Journal of Parallel Programming, vol. 18, pp. 365–400, 1989.J. Camilleri, “An operational semantics for OCCAM,” International Journal of Parallel Programming, vol. 18, pp. 365–400, 1989.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.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.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.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.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.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.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.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.T. Nipkow and G. Klein, Concrete semantics: with Isabelle/HOL. Springer, 2014.T. Nipkow and G. Klein, Concrete semantics: with Isabelle/HOL. Springer, 2014.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.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.M. Norrish, “C formalised in HOL,” University of Cambridge, Computer Laboratory, UCAM-CL-TR-453, 1998.M. Norrish, “C formalised in HOL,” University of Cambridge, Computer Laboratory, UCAM-CL-TR-453, 1998.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.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.G. J. Smeding, “An executable operational semantics for Python,” mathesis, Universiteit Utrecht, 2009. Available: http://gideon.smdng.nl/wp-content/uploads/thesis.pdfG. J. Smeding, “An executable operational semantics for Python,” mathesis, Universiteit Utrecht, 2009. Available: http://gideon.smdng.nl/wp-content/uploads/thesis.pdfM. A. K"ohl, “An executable structural operational formal semantics for Python.” 2021.M. A. K"ohl, “An executable structural operational formal semantics for Python.” 2021.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.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.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.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.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.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.D. Youn et al., “Bringing the WebAssembly Standard up to Speed with SpecTec,” vol. 8, no. PLDI, p. 210, 2024, doi: 10.1145/3656440.D. Youn et al., “Bringing the WebAssembly Standard up to Speed with SpecTec,” vol. 8, no. PLDI, p. 210, 2024, doi: 10.1145/3656440.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.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.

The authors declare that there are no conflicts of interest present.