<abstract xmlns="http://www.w3.org/1999/xhtml">This paper continues formalization in Mizar <xref ref-type="bibr" rid="j_forma-2018-0011_ref_002_w2aab3b7b3b1b6b1ab1ab2Aa">[2</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_001_w2aab3b7b3b1b6b1ab1ab1Aa">1</xref>] of basic notions of the composition-nominative approach to program semantics <xref ref-type="bibr" rid="j_forma-2018-0011_ref_013_w2aab3b7b3b1b6b1ab1ac13Aa">[13]</xref> which was started in <xref ref-type="bibr" rid="j_forma-2018-0011_ref_008_w2aab3b7b3b1b6b1ab1ab8Aa">[8</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_011_w2aab3b7b3b1b6b1ab1ac11Aa">11]</xref>.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 [<xref ref-type="bibr" rid="j_forma-2018-0011_ref_004_w2aab3b7b3b1b6b1ab1ab4Aa">4</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_006_w2aab3b7b3b1b6b1ab1ab6Aa">6</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_007_w2aab3b7b3b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_005_w2aab3b7b3b1b6b1ab1ab5Aa">5</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_003_w2aab3b7b3b1b6b1ab1ab3Aa">3</xref>].In the paper we introduce a definition of the notion of a binominative function over a set <italic>D</italic> understood as a partial function which maps elements of <italic>D</italic> to <italic>D</italic>. The sets of binominative functions and nominative predicates <xref ref-type="bibr" rid="j_forma-2018-0011_ref_011_w2aab3b7b3b1b6b1ab1ac11Aa">[11]</xref> over given sets form the carrier of the generalized Glushkov algorithmic algebra <xref ref-type="bibr" rid="j_forma-2018-0011_ref_014_w2aab3b7b3b1b6b1ab1ac14Aa">[14]</xref>. 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 <xref ref-type="bibr" rid="j_forma-2018-0011_ref_010_w2aab3b7b3b1b6b1ab1ac10Aa">[10</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_012_w2aab3b7b3b1b6b1ab1ac12Aa">12</xref>, <xref ref-type="bibr" rid="j_forma-2018-0011_ref_009_w2aab3b7b3b1b6b1ab1ab9Aa">9]</xref>.</abstract>

This paper continues formalization in Mizar [2, 1] of basic notions of the composition-nominative approach to program semantics [13] which was started in [8, 11].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 [4, 6, 7, 5, 3].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 [11] over given sets form the carrier of the generalized Glushkov algorithmic algebra [14]. 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 [10, 12, 9].

On Algebras of Algorithms and Specifications over Uninterpreted Data

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"On Algebras of Algorithms and Specifications over Uninterpreted Data"}

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

On Algebras of Algorithms and Specifications over Uninterpreted Data

Data publikacji: 24 gru 2018

Zakres stron: 141 - 147

Przyjęty: 29 cze 2018

DOI: https://doi.org/10.2478/forma-2018-0011

Słowa kluczowe
Glushkov algorithmic algebra, uninterpreted data

© 2018 Ievgen Ivanov et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

On Algebras of Algorithms and Specifications over Uninterpreted Data

Data publikacji: 24 gru 2018

Zakres stron: 141 - 147

Przyjęty: 29 cze 2018

DOI: https://doi.org/10.2478/forma-2018-0011

Słowa kluczoweGlushkov algorithmic algebra, uninterpreted data

© 2018 Ievgen Ivanov et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Słowa kluczowe
Glushkov algorithmic algebra, uninterpreted data