author = {Andrii Kryvolap and Mykola Nikitchenko and Wolfgang Schreiner},
title = {{Extending Floyd-Hoare Logic for Partial Pre- and Postconditions}},
booktitle = {{ ICTERI 2013: 9th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Kherson, Ukraine, June 19-22, 2013, Revised Selected Papers}},
language = {english},
abstract = {Traditional (classical) Floyd-Hoare logic is defined for a case of total pre- and postconditions while programs can be partial. In the chapter we propose to extend this logic for partial conditions. To do this we first construct and investigate special program algebras of partial predicates, functions, and programs. In such algebras program correctness assertions are presented with the help of a special composition called Floyd-Hoare composition. This composition is monotone and continuous. Considering the class of constructed algebras as a semantic base we then define an extended logic – Partial Floyd-Hoare Logic – and investigate its properties. This logic has rather complicated soundness constraints for inference rules, therefore simpler sufficient constraints are proposed. The logic constructed can be used for program verification.},
series = {Communications in Computer and Information Science},
pages = {0--23},
publisher = {Springer},
address = {Berlin},
isbn_issn = {ISBN 978-3-319-03997-8 (Print) 978-3-319-03998-5 (Online)},
year = {2013},
editor = {Vadim Ermolayev et al},
refereed = {yes},
keywords = {Program algebra, program logic, partial predicate, soundness, composition- nominative approach},
length = {24}