Extending Floyd-Hoare Logic for Partial Pre- and Postconditions

作者: Andrii Kryvolap , Mykola Nikitchenko , Wolfgang Schreiner

DOI: 10.1007/978-3-319-03998-5_18

关键词:

摘要: 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 partial conditions. To do first construct investigate special program algebras predicates, functions, programs. such correctness assertions are presented with help composition called composition. This monotone continuous. Considering class constructed as semantic base then define an extended – Partial Logic its properties. has rather complicated soundness constraints inference rules, therefore simpler sufficient proposed. The used verification.

参考文章(36)
Mykola S. Nikitchenko, Valentyn G. Tymofieiev, Satisfiability and Validity Problems in Many-Sorted Composition-Nominative Pure Predicate Logics international conference on application of information and communication technologies. pp. 89- 110 ,(2012) , 10.1007/978-3-642-35737-4_6
Arnon Avron, Anna Zamansky, Non-Deterministic Semantics for Logical Systems Handbook of Philosophical Logic. pp. 227- 304 ,(2011) , 10.1007/978-94-007-0479-4_4
Horst Reichel, Initial computability, algebraic specifications, and partial algebras Oxford University Press, Inc.. ,(1987)
Andrzej Tarlecki, Beata Konikowska, Andrzej Blikle, A Three-Valued Logic for Software Specification and Validation. Tertium tamen datur Fundamenta Informaticae. ,vol. 14, pp. 411- 453 ,(1991) , 10.3233/FI-1991-14403
Merrie Bergmann, An Introduction to Many-Valued and Fuzzy Logic Cambridge University Press. ,(2008) , 10.1017/CBO9780511801129
Flemming Nielson, Hanne Riis Nielson, Semantics With Applications: A Formal Introduction ,(1992)
Beata Konikowska, Andrzej Tarlecki, Andrzej Blikle, A three-valued logic for software specification and validation Proceedings of the 2nd VDM-Europe Symposium on VDM---The Way Ahead. pp. 218- 242 ,(1988) , 10.1007/3-540-50214-9_19
Hans-Jörg Kreowski, Partial Algebras Flow From Algebraic Specifications international colloquium on automata languages and programming. pp. 521- 530 ,(1987) , 10.1007/3-540-18088-5_45
Ralph-Johan J. Back, D. Gries, F. B. Schneider, Refinement Calculus: A Systematic Introduction ,(1998)