Andrii Kryvolap, Mykola Nikitchenko, Wolfgang Schreiner,
"Extending Floyd-Hoare Logic for Partial Pre- and Postconditions"
, in Vadim Ermolayev et al: 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, Serie Communications in Computer and Information Science, Springer, Berlin, Seite(n) 0--23, 2013, ISBN: 978-3-319-03997-8
Extending Floyd-Hoare Logic for Partial Pre- and Postconditions
Sprache des Titels:
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
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.
Sprache der Kurzfassung:
Communications in Computer and Information Science