@inproceedings{8b81d6d6bedb4cb180c62b82e5d1b26b,
title = "Extending Floyd-Hoare Logic for Partial Pre- and Postconditions",
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.",
author = "Andrii Kryvolap and Mykola Nikitchenko and Wolfgang Schreiner",
year = "2013",
doi = "10.1007/978-3-319-03998-5\_18",
language = "English",
isbn = "978-3-319-03997-8",
series = "Communications in Computer and Information Science",
publisher = "Springer",
pages = "355--378",
editor = "\{Vadim Ermolayev et al\}",
booktitle = "ICTERI 2013: 9th Internat. Conf. on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Kherson, UKR, June 19-22, 2013, Revised Selected Papers",
}