RO  EN
IMI/Publicaţii/CSJM/Ediţii/CSJM v.24, n.3 (72), 2016/

Proving Properties of Programs on Hierarchical Nominative Data

Authors: Ievgen Ivanov, Mykola Nikitchenko, Volodymyr G. Skobelev
Keywords: Programming language semantics, algorithmic algebras, nominative data, composition, Friedman scheme.

Abstract

In the paper we develop methods for proving properties of programs on hierarchical nominative data on the basis of the composition-nominative approach. In accordance with this approach, the semantics of a program is a function on nominative data constructed from basic operations using compositions (operations on functions) which represent programming language constructs. Nominative data can be considered as a class of abstract data models which is able to represent many concrete types of structured and semistructured data that appear in programming. Thus, proofs of properties of programs depend on proofs of properties of compositions and basic operations on nominative data.

To simplify the parts of such proofs that deal with program compositions we propose to represent compositions of programs on nominative data using effective definitional schemes of H. Friedman. This permits us to consider proofs in data algebras (which are simpler to derive, automate, etc.) instead of proofs in program algebras. In particular, we demonstrate that the properties of programs related to structural transformations of data can be reduced to the data level. The obtained results can be used in software development and verification.

Ievgen Ivanov
Taras Shevchenko National University of Kyiv
64/13 Volodymyrska Street, 01601 Kyiv, Ukraine
Phone: +380442590519
E-mail:

Mykola Nikitchenko
Taras Shevchenko National University of Kyiv
64/13 Volodymyrska Street, 01601 Kyiv, Ukraine
Phone: +380442590519
E-mail:

Volodymyr G. Skobelev
V.M. Glushkov Institute of Cybernetics of NAS of Ukraine
40 Glushkova ave., Kyiv, Ukraine, 03187
Phone: +380634318605
E-mail:

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License

Fulltext

Adobe PDF document0.19 Mb