Andrii Kryvolap, Mykola Nikitchenko, Wolfgang Schreiner,
"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: ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013, Serie CEUR-WS.org CEUR Workshop Proceedings, Vol. 1000, CEUR-WS.org, Seite(n) 533-549, 6-2013, ISBN: 1613-0073
Program Algebras with Monotone Floyd-Hoare Composition
Sprache des Titels:
ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013
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