Institutul de Matematică şi Informatică "Vladimir Andrunachievici"
Universitatea de Stat din MoldovaProving Properties of Programs on Hierarchical Nominative Data
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.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:
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License
Fulltext
– 0.19 Mb
Contents
- Propositional inquisitive logic: a survey
- "The absence of the difference from a pot is potness" - Axiomatic Proofs of Theorems Concerning Negative Properties in Navya-Nyāya
- About Applications of Distances on Monoids of Strings
- Insertion Modeling and Its Applications
- Proving Properties of Programs on Hierarchical Nominative Data
- Natural Language Processing versus Logic. Pros and cons on the dispute whether logic is useful in the computational interpretation of language
- Executable choreographies applied in OPERANDO
