<abstract xmlns="http://www.w3.org/1999/xhtml">In this paper we give a formal definition of the notion of nominative data with simple names and complex values [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_015_w2aab3b7b4b1b6b1ab1ac15Aa">15</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_016_w2aab3b7b4b1b6b1ab1ac16Aa">16</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>] and formal definitions of the basic operations on such data, including naming, denaming and overlapping, following the work [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>].The notion of nominative data plays an important role in the composition-nominative approach to program formalization [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_015_w2aab3b7b4b1b6b1ab1ac15Aa">15</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_016_w2aab3b7b4b1b6b1ab1ac16Aa">16</xref>] which is a development of composition programming [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_018_w2aab3b7b4b1b6b1ab1ac18Aa">18</xref>]. Both approaches are compared in [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_014_w2aab3b7b4b1b6b1ab1ac14Aa">14</xref>].The composition-nominative approach considers mathematical models of computer software and data on various levels of abstraction and generality and provides mathematical tools for reasoning about their properties. In particular, nominative data are mathematical models of data which are stored and processed in computer systems. The composition-nominative approach considers different types [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_014_w2aab3b7b4b1b6b1ab1ac14Aa">14</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>] of nominative data, but all of them are based on the name-value relation. One powerful type of nominative data, which is suitable for representing many kinds of data commonly used in programming like lists, multidimensional arrays, trees, tables, etc. is the type of nominative data with simple (abstract) names and complex (structured) values. The set of nominative data of given type together with a number of basic operations on them like naming, denaming and overlapping [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>] form an algebra which is called <italic>data algebra</italic>.In the composition-nominative approach computer programs which process data are modeled as partial functions which map nominative data from the carrier of a given data algebra (input data) to nominative data (output data). Such functions are also called <italic>binominative functions</italic>. Programs which evaluate conditions are modeled as partial predicates on nominative data (nominative predicates). Programming language constructs like sequential execution, branching, cycle, etc. which construct programs from the existing programs are modeled as operations which take binominative functions and predicates and produce binominative functions. Such operations are called <italic>compositions</italic>. A set of binominative functions and a set of predicates together with appropriate compositions form an algebra which is called <italic>program algebra</italic>. This algebra serves as a semantic model of a programming language.For functions over nominative data a special computability called abstract computability is introduces and complete classes of computable functions are specified [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_016_w2aab3b7b4b1b6b1ab1ac16Aa">16</xref>].For reasoning about properties of programs modeled as binominative functions a Floyd-Hoare style logic [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_001_w2aab3b7b4b1b6b1ab1ab1Aa">1</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_002_w2aab3b7b4b1b6b1ab1ab2Aa">2</xref>] is introduced and applied [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_012_w2aab3b7b4b1b6b1ab1ac12Aa">12</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_013_w2aab3b7b4b1b6b1ab1ac13Aa">13</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_008_w2aab3b7b4b1b6b1ab1ab8Aa">8</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_011_w2aab3b7b4b1b6b1ab1ac11Aa">11</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_009_w2aab3b7b4b1b6b1ab1ab9Aa">9</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_010_w2aab3b7b4b1b6b1ab1ac10Aa">10</xref>]. One advantage of this approach to reasoning about programs is that it naturally handles programs which process complex data structures (which can be quite straightforwardly represented as nominative data). Also, unlike classical Floyd-Hoare logic, the mentioned logic allows reasoning about assertions which include partial pre- and post-conditions [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_011_w2aab3b7b4b1b6b1ab1ac11Aa">11</xref>].Besides modeling data processed by programs, nominative data can be also applied to modeling data processed by signal processing systems in the context of the mathematical systems theory [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_004_w2aab3b7b4b1b6b1ab1ab4Aa">4</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_006_w2aab3b7b4b1b6b1ab1ab6Aa">6</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_007_w2aab3b7b4b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_005_w2aab3b7b4b1b6b1ab1ab5Aa">5</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_003_w2aab3b7b4b1b6b1ab1ab3Aa">3</xref>].</abstract>

In this paper we give a formal definition of the notion of nominative data with simple names and complex values [15, 16, 19] and formal definitions of the basic operations on such data, including naming, denaming and overlapping, following the work [19].The notion of nominative data plays an important role in the composition-nominative approach to program formalization [15, 16] which is a development of composition programming [18]. Both approaches are compared in [14].The composition-nominative approach considers mathematical models of computer software and data on various levels of abstraction and generality and provides mathematical tools for reasoning about their properties. In particular, nominative data are mathematical models of data which are stored and processed in computer systems. The composition-nominative approach considers different types [14, 19] of nominative data, but all of them are based on the name-value relation. One powerful type of nominative data, which is suitable for representing many kinds of data commonly used in programming like lists, multidimensional arrays, trees, tables, etc. is the type of nominative data with simple (abstract) names and complex (structured) values. The set of nominative data of given type together with a number of basic operations on them like naming, denaming and overlapping [19] form an algebra which is called data algebra.In the composition-nominative approach computer programs which process data are modeled as partial functions which map nominative data from the carrier of a given data algebra (input data) to nominative data (output data). Such functions are also called binominative functions. Programs which evaluate conditions are modeled as partial predicates on nominative data (nominative predicates). Programming language constructs like sequential execution, branching, cycle, etc. which construct programs from the existing programs are modeled as operations which take binominative functions and predicates and produce binominative functions. Such operations are called compositions. A set of binominative functions and a set of predicates together with appropriate compositions form an algebra which is called program algebra. This algebra serves as a semantic model of a programming language.For functions over nominative data a special computability called abstract computability is introduces and complete classes of computable functions are specified [16].For reasoning about properties of programs modeled as binominative functions a Floyd-Hoare style logic [1, 2] is introduced and applied [12, 13, 8, 11, 9, 10]. One advantage of this approach to reasoning about programs is that it naturally handles programs which process complex data structures (which can be quite straightforwardly represented as nominative data). Also, unlike classical Floyd-Hoare logic, the mentioned logic allows reasoning about assertions which include partial pre- and post-conditions [11].Besides modeling data processed by programs, nominative data can be also applied to modeling data processed by signal processing systems in the context of the mathematical systems theory [4, 6, 7, 5, 3].

Simple-Named Complex-Valued Nominative Data – Definition and Basic Operations

Formalized Mathematics

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

In this paper we give a formal definition of the notion of nominative data with simple names and complex values [15, 16, 19] and formal definitions of the...

Simple-Named Complex-Valued Nominative Data – Definition and Basic Operations

Data publikacji: 19 gru 2017

Zakres stron: 205 - 216

Otrzymano: 30 sie 2017

DOI: https://doi.org/10.1515/forma-2017-0020

Słowa kluczowe
program semantics, software verification, nominative data

© 2017 Ievgen Ivanov et al., published by De Gruyter Open

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

Simple-Named Complex-Valued Nominative Data – Definition and Basic Operations

Data publikacji: 19 gru 2017

Zakres stron: 205 - 216

Otrzymano: 30 sie 2017

DOI: https://doi.org/10.1515/forma-2017-0020

Słowa kluczoweprogram semantics, software verification, nominative data

© 2017 Ievgen Ivanov et al., published by De Gruyter Open

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

Słowa kluczowe
program semantics, software verification, nominative data