mireabulletinRussian Technological JournalRussian Technological Journal2782-32102500-316XRTU MIREA10.32362/2500-316X-2022-10-1-18-27mireabulletin-451Research ArticleИНФОРМАЦИОННЫЕ СИСТЕМЫ. ИНФОРМАТИКА. ПРОБЛЕМЫ ИНФОРМАЦИОННОЙ БЕЗОПАСНОСТИINFORMATION SYSTEMS. COMPUTER SCIENCES. ISSUES OF INFORMATION SECURITYЭквивалентность схем программ на основе алгебраического подхода к заданию семантики языков программированияEquivalence of the schemes of programs based on the algebraic approach to setting the semantics of programming languagesКораблинЮ. П.KorablinY. P.

Кораблин Юрий Прокофьевич, д.т.н., профессор, профессор кафедры прикладной математики и искусственного интеллекта Института информационных и вычислительных технологийScopus Author ID 6603265252 

111250, Россия, Москва, Красноказарменная ул., д. 14

Yuri P. Korablin, Dr. Sci (Eng.), Professor, Professor, Department of Applied Mathematics and Artificial Intelligence, Institute of Information and Computational Technologies

111250, Moscow, Krasnokazarmennaya ul., 14

KorablinYP@mpei.ruНИУ МЭИРоссияNRU MPEIRussian Federation2022270220221011827Copyright © Кораблин Ю.П., 20222022Кораблин Ю.П.Korablin Y.P.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.rtj-mirea.ru/jour/article/view/451

Цели. Статья посвящена вопросам эквивалентности схем программ. В соответствии с работами А.А. Ляпунова и Ю.И. Янова – основоположников данной теории, под схемой программы понимается ее модель, в которой осуществляется абстрагирование от содержательных значений операторов и выражений. При этом неизменной остается структура программы, включающая символические обозначения операторов и выражений при сохранении последовательности их выполнения. Представленная в статье модель языка программирования содержит основные конструкции последовательных языков и является ядром имеющихся языков последовательного программирования. Цель работы – разработка эффективного алгоритма исследования вопросов эквивалентности (неэквивалентности) схем программ последовательных языков программирования.Методы. Используется алгебраический подход к заданию семантики языков программирования для исследования вопросов эквивалентности схем программ.Результаты. Предложен новый алгебраический подход к заданию формальной семантики языков последовательного программирования – процессная семантика. Процессная семантика задается посредством сопоставления программам (схемам программ) множества вычислительных последовательностей. Под вычислительной последовательностью понимается последовательность выполнения действий (команд и тестов) программы. На введенной семантической области (множестве вычислительных последовательностей) определены операции конкатенации двух видов (тест-команда и команда-команда) и операция объединения, свойства которых заданы системами аксиом. Доказана конечность представления семантических значений в виде систем рекурсивных уравнений. Предложен алгоритм доказательства эквивалентности (неэквивалентности) систем рекурсивных уравнений, характеризующих семантические значения для пары схем программ, откуда вытекает эквивалентность (неэквивалентности) программ в сильном смысле.Выводы. Показана эффективность применения предложенного алгоритма для доказательства эквивалентности схем последовательных программ, в которых отсутствует побочный эффект при вычислении выражений, т.е. последовательное вычисление выражения более, чем один раз, ничего не меняет. В статье приведен демонстрационный пример доказательства эквивалентности схем программ двумя методами: известным методом индукции фиксированной точки де Баккера – Скотта и предложенным в статье методом. Сравнение приведенных методов свидетельствует не только об эффективности нового метода, но и его существенной простоте, что было подтверждено на практике при выполнении соответствующих заданий студентами специальности «Прикладная математика и информатика» Национального исследовательского университета МЭИ в процессе изучения дисциплины «Семантика языков программирования».

Objectives. The paper deals with the equivalence of program schemes. According to A.A. Lyapunov and Yu.I. Yanov, the founders of this theory, a program scheme is understood as a program model wherein abstraction from contensive values of operators and expressions is performed. In this case, the program structure containing symbolic notation of operators and expressions remains unchanged while maintaining their execution sequence. The programming language model presented in the paper contains basic constructs of sequential languages and is the core of the existing sequential programming languages. The paper aimed at developing an effective algorithm for studying equivalence (nonequivalence) of program schemes of sequential programming languages.Methods. An algebraic approach to specifying semantics of programming languages was used for studying the equivalence of program schemes.Results. A process semantics being the new algebraic approach to specifying the formal semantics of sequential programming languages was proposed. The process semantics was specified by matching programs (program schemes) with a set of computation sequences. The computation sequence was understood as the execution sequence of actions (commands and tests) of the program. Two types of concatenation operations (test–command and command–command) and the merge operation, which properties are given by axiomatic systems, were defined in the introduced semantic domain. The finiteness of the semantic value representation in the form of systems of recursive equations was proved. The algorithm for proving the equivalence (nonequivalence) of systems of recursive equations characterizing semantic values for a pair of program schemes was proposed, which implies the equivalence (nonequivalence) of programs in the strong sense.Conclusions. The paper demonstrates the efficient use of the proposed algorithm for proving the equivalence of sequential program schemes excluding side effects when calculating expressions, i.e., sequential computation of the expression more than once does not change anything. The example of proving the equivalence of program schemes by two methods—the well-known de Bakker–Scott fixed-point induction method and the method proposed by the author—is given. Comparison of the above methods testifies not only to the new method′s effectiveness but also to its significant simplicity, proved in practice by students who performed corresponding tasks when studying the Semantics of Programming Languages at the Institute of Information and Computing Technologies at the National Research University Moscow Power Engineering Institute (Moscow, Russia).

схема программысемантические областипроцессная семантикаэквациональная характеризация семантических значений программэквивалентность схем программprogram schemesemantic domainsprocess semanticsequational characterization of the semantic meanings of programsequivalence of program schemesReferencesКораблин Ю.П., Куликова Н.Л., Шипов А.А. Программы как минимальные фиксированные точки: теоретические и прикладные аспекты. Cloud of Science. 2020;7(3):535−550.Korablin Yu.P., Kulikova N.L., Shipov A.A. Programs as least fixed points: theoretical and applied aspects. Cloud of Science. 2020;7(3):535−550 (in Russ.).Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург; 2010. 610 с. ISBN 978-5-9775-0404-1Karpov Yu.G. Model checking. Verifikatsiya parallel’nykh i raspredelennykh programmnykh system (Model checking. Verification of parallel and distributed software systems). St. Petersburg: BHV-Petersburg; 2010. 610 p. (in Russ.). ISBN 978-5-9775-0404-1Кораблин Ю.П., Кучугуров И.В. Процессная семантика языков распределенного программирования. Программные продукты и системы. 2011;4(96):57−64.Korablin Yu.P., Kuchugurov I.V. Process semantics of distributed programming language. Programmnye produkty i sistemy = Software & Systems. 2011;4(96):57−64 (in Russ.).Кораблин Ю.П. Семантические методы анализа программ. М.: Изд-во МЭИ; 2019. 68 с. ISBN 978-5-7046-2173-7Korablin Yu.P. Semanticheskie metody analiza programm (Semantic methods of program analysis). Moscow: MEI; 2019. 68 p. (in Russ.). ISBN 978-5-7046-2173-7Floyd R.W. Assigning Meanings to Programs. In: Colburn T.R., Fetzer J.H., Rankin T.L. (Eds.). Program Verification. Studies in Cognitive Systems. Dordrecht: Springer; 1993. V. 14. P. 65−81. https://doi.org/10.1007/978-94-011-1793-7_4Floyd R.W. Assigning meanings to programs. In: Colburn T.R., Fetzer J.H., Rankin T.L. (Eds.). Program Verification. Studies in Cognitive Systems. Dordrecht: Springer; 1993. V. 14. P. 65−81. https://doi.org/10.1007/978-94-011-1793-7_4Hoare C.A.R., Wirth N. An axiomatic definition of the programming language PASCAL. Acta Informatica. 1973;2(4):335−355. https://doi.org/10.1007/BF00289504Hoare C.A.R., Wirth N. An axiomatic definition of the programming language PASCAL. Acta Informatica. 1973;2(4):335−355. https://doi.org/10.1007/BF00289504Stoy J.E. Denotational semantics: The Scott-Strachey approach to programming language theory. Cambridge: The MIT Press Series in Computer Science; 1985. 414 p.Stoy J.E. Denotational semantics: The Scott-Strachey approach to programming language theory. Cambridge: The MIT Press Series in Computer Science; 1985. 414 p.Алагич С., Арбиб M. Проектирование корректных структурированных программ: пер. с англ. M.: Радио и связь; 1984. 264 с.Alagich S., Arbib M. Proektirovanie korrektnykh strukturirovannykh programm (Designing correct structured programs): transl. from Eng. Moscow: Radio i svyaz’; 1984. 264 р. (in Russ.).de Bakker J. Mathematical Theory of Program Correctness. Prentice Hall International; 1980. 505 p.de Bakker J. Mathematical theory of program correctness. Prentice Hall International; 1980. 505 p.Захаров В.А. Моделирование и анализ поведения последовательных реагирующих программ. Труды Института системного программирования РАН. 2015:27(2):221−250. https://doi.org/10.15514/ISPRAS2015-27(2)-13Zakharov V.A. Modeling and analysis of the behavior of successive reactive programs. Trudy Instituta sistemnogo programmirovaniya RAN = Proceedings of the Institute for System Programming of the RAS. 2015;27(2):221−250 (in Russ.). https://doi.org/10.15514/ISPRAS-2015-27(2)-13Захаров В.А., Подымов В.В. Применение алгоритмов проверки эквивалентности для оптимизации программ. Труды Института системного программирования РАН. 2015;27(4):145−174. https://doi.org/10.15514/ISPRAS-2015-27(4)-8Zakharov V.A., Podymov V.V. On the application of equivalence checking algorithms for program minimization. Trudy Instituta sistemnogo programmirovaniya RAN = Proceedings of the Institute for System Programming of the RAS. 2015;27(4):145−174 (in Russ.). https://doi.org/10.15514/ISPRAS-2015-27(4)-8Захаров В.А., Жайлауова Ш.Р. О задаче минимизации последовательных программ. Моделирование и анализ информационных систем. 2017;24(7):415−433. https://doi.org/10.18255/1818-1015-2017-4-415-433Zakharov V.A., Zhailauova S.R. On the minimization problem for sequential programs. Modelirovanie i analiz informatsionnykh system = Modeling and Analysis of Information Systems. 2017;24(4):415−433 (in Russ.). https://doi.org/10.18255/1818-1015-2017-4-415-433Молчанов А.Э. Разрешимость проблемы эквивалентных преобразований в классе примитивных схем программ. Труды Института системного программирования РАН. 2015;27(2):173−188. https://doi.org/10.15514/ISPRAS-2015-27(2)-11Molchanov A.E. A Solution to the equivalent transformation problem in a class of primitive program schemes. Trudy Instituta sistemnogo programmirovaniya RAN = Proceedings of the Institute for System Programming of the RAS. 2015;27(2):173−188 (in Russ.). https://doi.org/10.15514/ISPRAS-2015-27(2)-11Кораблин Ю.П., Шипов А.А. Верификация моделей систем на базе эквациональной характеристики формул CTL. Программные продукты и системы. 2019;32(4):547−555. http://dx.doi.org/10.15827/0236-235X.128.547-555Korablin Yu.P., Shipov A.A. Systems model verification based on equational characteristics of СTL formulas. Programmnye produkty i sistemy = Software & Systems. 2019;32(4):547−555 (in Russ.). http://dx.doi.org/10.15827/0236-235X.128.547-555

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