## Summary

This paper continues formalization in Mizar , ] of basic notions of the composition-nominative approach to program semantics which was started in , .

The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory [, , , , ].

In the paper we introduce a definition of the notion of a binominative function over a set *D* understood as a partial function which maps elements of *D* to *D*. The sets of binominative functions and nominative predicates over given sets form the carrier of the generalized Glushkov algorithmic algebra . This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties.

We formalize the operations of this algebra (also called compositions) which are valid over uninterpretated data and which include among others the sequential composition, the prediction composition, the branching composition, the monotone Floyd-Hoare composition, and the cycle composition. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in , , .

uninterpreted data. Formalized Mathematics , 26( 2 ):141–147, 2018. doi:10.2478/forma-2018-0011. [12] Adrian Jaszczak. Partial correctness of a power algorithm. Formalized Mathematics , 27 ( 2 ):189–195, 2019. doi:10.2478/forma-2019-0018. [13] Adrian Jaszczak and Artur Korniłowicz. Partial correctness of a factorial algorithm. Formalized Mathematics , 27( 2 ):181–187, 2019. doi:10.2478/forma-2019-0017. [14] Artur Kornilowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. Formalization of the algebra of nominative data in Mizar. In Maria Ganzha, Leszek A

formalization in Mizar. The Computer Science Journal of Moldova , 26(1):59–76, 2018. [10] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On algebras of algorithms and specifications over uninterpreted data. Formalized Mathematics , 26( 2 ):141–147, 2018. doi:10.2478/forma-2018-0011. [11] Artur Kornilowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. Formalization of the algebra of nominative data in Mizar. In Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2017 Federated Conference on Computer Science and

, 26( 2 ):149–158, 2018. doi:10.2478/forma-2018-0012. [9] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized Mathematics , 26( 2 ): 159–164, 2018. doi:10.2478/forma-2018-0013. [10] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On algebras of algorithms and specifications over uninterpreted data. Formalized Mathematics , 26( 2 ):141–147, 2018. doi:10.2478/forma-2018-0011. [11] Artur Kornilowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov

uninterpreted data. Formalized Mathematics , 26( 2 ):141–147, 2018. doi:10.2478/forma-2018-0011. [12] Artur Kornilowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. Formalization of the algebra of nominative data in Mizar. In Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Prague, Czech Republic, September 3–6, 2017. , pages 237–244, 2017. ISBN 978-83-946253-7-5. doi:10.15439/2017F301. [13] Artur Kornilowicz, Andrii Kryvolap, Mykola