Equivalence of the schemes of programs based on the algebraic approach to setting the semantics of programming languages

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).

1. 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.).

2. Karpov 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

3. 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.).

4. Korablin Yu.P. Semanticheskie metody analiza programm (Semantic methods of program analysis). Moscow: MEI; 2019. 68 p. (in Russ.). ISBN 978-5-7046-2173-7

5. Floyd 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_4

6. Hoare 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/BF00289504

7. Stoy J.E. Denotational semantics: The Scott-Strachey approach to programming language theory. Cambridge: The MIT Press Series in Computer Science; 1985. 414 p.

8. Alagich S., Arbib M. Proektirovanie korrektnykh strukturirovannykh programm (Designing correct structured programs): transl. from Eng. Moscow: Radio i svyaz’; 1984. 264 р. (in Russ.).

9. de Bakker J. Mathematical theory of program correctness. Prentice Hall International; 1980. 505 p.

10. Zakharov 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

11. Zakharov 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

12. Zakharov 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

13. Molchanov 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

14. Korablin 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