Построение операционной семантики языков программирования в виде исполняемых онтологических моделей программ

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

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.