Conţinutul numărului revistei |
Articolul precedent |
Articolul urmator |
876 3 |
Ultima descărcare din IBN: 2017-04-25 22:49 |
Căutarea după subiecte similare conform CZU |
004.42:519.85 (3) |
Programe. Software (300) |
Cercetări operaționale (OR) teorii şi metode matematice (170) |
SM ISO690:2012 IVANOV, Ievgen, NIKITCHENKO, Mykola, SKOBELEV, Volodymyr. Proving Properties of Programs on Hierarchical Nominative Data. In: Computer Science Journal of Moldova, 2016, nr. 3(72), pp. 371-398. ISSN 1561-4042. |
EXPORT metadate: Google Scholar Crossref CERIF DataCite Dublin Core |
Computer Science Journal of Moldova | |||||||
Numărul 3(72) / 2016 / ISSN 1561-4042 /ISSNe 2587-4330 | |||||||
|
|||||||
CZU: 004.42:519.85 | |||||||
Pag. 371-398 | |||||||
|
|||||||
Descarcă PDF | |||||||
Rezumat | |||||||
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. |
|||||||
Cuvinte-cheie Programming language semantics, algorithmic algebras, nominative data, Friedman scheme, composition |
|||||||
|