Conţinutul numărului revistei |
Articolul precedent |
Articolul urmator |
882 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 (302) |
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 |
|||||||
|
DataCite XML Export
<?xml version='1.0' encoding='utf-8'?> <resource xmlns:xsi='http://www.w3.org/2001/XMLSchema-instance' xmlns='http://datacite.org/schema/kernel-3' xsi:schemaLocation='http://datacite.org/schema/kernel-3 http://schema.datacite.org/meta/kernel-3/metadata.xsd'> <creators> <creator> <creatorName>Ivanov, I.</creatorName> <affiliation>Universitatea Naţională „Taras Shevchenko“, Kiev, Ucraina</affiliation> </creator> <creator> <creatorName>Nikitcenko, M.</creatorName> <affiliation>Universitatea Naţională „Taras Shevchenko“, Kiev, Ucraina</affiliation> </creator> <creator> <creatorName>Skobelev, V.V.</creatorName> <affiliation>Institute of Cybernetics, National Academy of Sciences of Ukraine, Ucraina</affiliation> </creator> </creators> <titles> <title xml:lang='en'>Proving Properties of Programs on Hierarchical Nominative Data</title> </titles> <publisher>Instrumentul Bibliometric National</publisher> <publicationYear>2016</publicationYear> <relatedIdentifier relatedIdentifierType='ISSN' relationType='IsPartOf'>1561-4042</relatedIdentifier> <subjects> <subject>Programming language semantics</subject> <subject>algorithmic algebras</subject> <subject>nominative data</subject> <subject>composition</subject> <subject>Friedman scheme</subject> <subject schemeURI='http://udcdata.info/' subjectScheme='UDC'>004.42:519.85</subject> </subjects> <dates> <date dateType='Issued'>2016-10-11</date> </dates> <resourceType resourceTypeGeneral='Text'>Journal article</resourceType> <descriptions> <description xml:lang='en' descriptionType='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. </description> </descriptions> <formats> <format>application/pdf</format> </formats> </resource>