Program Algebras with Monotone Floyd-Hoare Composition

Andrii Kryvolap; Mykola Nikitchenko; Wolfgang Schreiner

Program Algebras with Monotone Floyd-Hoare Composition

Andrii Kryvolap, Mykola Nikitchenko, Wolfgang Schreiner

Research Institute for Symbolic Computation

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

In the paper special program algebras of partial predicates and functions are described. Such algebras form a semantic component of a modified Floyd-Hoare logic constructed on the base of a composition-nominative approach. According to this approach, Floyd-Hoare assertions are presented with the help of a special composition called Floyd-Hoare composition. Monotonicity and continuity of this composition are proved. The language of the modified Floyd-Hoare logic is described. Further, the inference rules for such logic are studied, their soundness conditions are specified. The logic constructed can be used for program verification. Keywords. Program algebra, program logic, composition-nominative

Original language	English
Title of host publication	ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013
Editors	Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko
Publisher	CEUR-WS.org
Pages	533-549
Number of pages	17
Volume	1000
Publication status	Published - Jun 2013

Publication series

Name	CEUR-WS.org CEUR Workshop Proceedings
ISSN (Print)	1613-0073

Fields of science

101001 Algebra
101002 Analysis
101 Mathematics
102 Computer Sciences
102011 Formal languages
101009 Geometry
101013 Mathematical logic
101020 Technical mathematics
101025 Number theory
101012 Combinatorics
101005 Computer algebra
101006 Differential geometry
101003 Applied geometry
102025 Distributed systems

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

Kryvolap, A., Nikitchenko, M., & Schreiner, W. (2013). Program Algebras with Monotone Floyd-Hoare Composition. In Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko (Ed.), ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013 (Vol. 1000, pp. 533-549). (CEUR-WS.org CEUR Workshop Proceedings). CEUR-WS.org.

Kryvolap, Andrii ; Nikitchenko, Mykola ; Schreiner, Wolfgang. / Program Algebras with Monotone Floyd-Hoare Composition. ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013. editor / Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko. Vol. 1000 CEUR-WS.org, 2013. pp. 533-549 (CEUR-WS.org CEUR Workshop Proceedings).

@inproceedings{cdd1618428224a32b7ad7c13d3c5bcf4,

title = "Program Algebras with Monotone Floyd-Hoare Composition",

abstract = "In the paper special program algebras of partial predicates and functions are described. Such algebras form a semantic component of a modified Floyd-Hoare logic constructed on the base of a composition-nominative approach. According to this approach, Floyd-Hoare assertions are presented with the help of a special composition called Floyd-Hoare composition. Monotonicity and continuity of this composition are proved. The language of the modified Floyd-Hoare logic is described. Further, the inference rules for such logic are studied, their soundness conditions are specified. The logic constructed can be used for program verification. Keywords. Program algebra, program logic, composition-nominative",

author = "Andrii Kryvolap and Mykola Nikitchenko and Wolfgang Schreiner",

year = "2013",

month = jun,

language = "English",

volume = "1000",

series = "CEUR-WS.org CEUR Workshop Proceedings",

publisher = "CEUR-WS.org",

pages = "533--549",

editor = "{Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko}",

booktitle = "ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013",

}

Kryvolap, A, Nikitchenko, M & Schreiner, W 2013, Program Algebras with Monotone Floyd-Hoare Composition. in Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko (ed.), ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013. vol. 1000, CEUR-WS.org CEUR Workshop Proceedings, CEUR-WS.org, pp. 533-549.

Program Algebras with Monotone Floyd-Hoare Composition. / Kryvolap, Andrii; Nikitchenko, Mykola; Schreiner, Wolfgang.
ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013. ed. / Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko. Vol. 1000 CEUR-WS.org, 2013. p. 533-549 (CEUR-WS.org CEUR Workshop Proceedings).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Program Algebras with Monotone Floyd-Hoare Composition

AU - Kryvolap, Andrii

AU - Nikitchenko, Mykola

AU - Schreiner, Wolfgang

PY - 2013/6

Y1 - 2013/6

N2 - In the paper special program algebras of partial predicates and functions are described. Such algebras form a semantic component of a modified Floyd-Hoare logic constructed on the base of a composition-nominative approach. According to this approach, Floyd-Hoare assertions are presented with the help of a special composition called Floyd-Hoare composition. Monotonicity and continuity of this composition are proved. The language of the modified Floyd-Hoare logic is described. Further, the inference rules for such logic are studied, their soundness conditions are specified. The logic constructed can be used for program verification. Keywords. Program algebra, program logic, composition-nominative

AB - In the paper special program algebras of partial predicates and functions are described. Such algebras form a semantic component of a modified Floyd-Hoare logic constructed on the base of a composition-nominative approach. According to this approach, Floyd-Hoare assertions are presented with the help of a special composition called Floyd-Hoare composition. Monotonicity and continuity of this composition are proved. The language of the modified Floyd-Hoare logic is described. Further, the inference rules for such logic are studied, their soundness conditions are specified. The logic constructed can be used for program verification. Keywords. Program algebra, program logic, composition-nominative

M3 - Conference proceedings

VL - 1000

T3 - CEUR-WS.org CEUR Workshop Proceedings

SP - 533

EP - 549

BT - ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013

A2 - Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko, null

PB - CEUR-WS.org

ER -

Kryvolap A, Nikitchenko M, Schreiner W. Program Algebras with Monotone Floyd-Hoare Composition. In Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko, editor, ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013. Vol. 1000. CEUR-WS.org. 2013. p. 533-549. (CEUR-WS.org CEUR Workshop Proceedings).