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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Floyd, R.W.: Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19, 19–31 (1967)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM (12), 576–580 (1969)
Nikitchenko, M.S., Shkilniak, S.S.: Mathematical logic and theory of algorithms. Publishing house of Taras Shevchenko National University of Kyiv, Kyiv (2008) (in Ukrainian)
Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction, p. 240. John Wiley & Sons Inc. (1992)
Nikitchenko, M.S., Tymofieiev, V.G.: Satisfiability in Composition-Nominative Logics. Central European Journal of Computer Science 2(3), 194–213 (2012)
Avron, A., Zamansky, A.: Non-Deterministic Semantics for Logical Systems. Handbook of Philosophical Logic 16, 227–304 (2011)
Nikitchenko, M., Tymofieiev, V.: Satisfiability and Validity Problems in Many-sorted Composition-Nominative Pure Predicate Logics. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2012. CCIS, vol. 347, pp. 89–110. Springer, Heidelberg (2013)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Schmidt, D.A.: Denotational Semantics – A Methodology for Language Development. Allyn and Bacon, Boston (1986)
Scott, D., Strachey, C.: Towards a Mathematical Semantics for Computer Languages. In: Proc. Symp. on Computers and Automata, Polytechnic Institute of Brooklyn; also Tech. Mon. PRG-6, pp. 19–46. Oxford U. Computing Lab. (1971)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, London (1998)
Boute, R.T.: Calculational Semantics: Deriving Programming Theories from Equations by Functional Predicate Calculus. ACM Transactions on Programming Languages and Systems 28(4), 747–793 (2006)
Wang, H.: The Calculus of Partial Predicates and Its Extension to Set Theory. Zeitschr. F. Math. Logik und Grundlagen D. Math. 7, 283–288 (1961)
Łukasiewicz, J.: O logice trójwartościowej. In: Borkowski, L. (ed.) Ruch Filozoficzny 5:170–171. English Translation: On Three-Valued Logic. Selected works by Jan Łu-kasiewicz, pp. 87–88. North–Holland, Amsterdam (1970)
Kleene, S.C.: On Notation for Ordinal Numbers. Journal Symbolic Logic 3, 150–155 (1938)
Bochvar, D.A.: On a 3-valued Logical Calculus and its Application to the Analysis of Contradictions. Matematiceskij Sbornik 4, 287–308 (1939) (in Russian)
Bergmann, M.: An Introduction to Many-Valued and Fuzzy Logic: Semantics, Algebras, and Derivation Systems. Cambridge University Press, Cambridge (2008)
Moisil, G.: Recherches sur les logiques nonchrysippiennes. Ann. Sci. Univ. Jassy 26, 431–436 (1940)
McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Braffort, P., Hirshberg, D. (eds.) Computer Programming and Formal Systems, pp. 33–70. North-Holland, Amsterdam (1963)
Bergstra, J.A., Ponse, A.: Bochvar-McCarthy Logic and Process Algebra. Notre Dame Journal of Formal Logic 39(4), 464–484 (1988)
Blikle, A.: Three-Valued Predicates for Software Specification and Validation. In: Bloomfield, R.E., Jones, R.B., Marshall, L.S. (eds.) VDM 1988. LNCS, vol. 328, pp. 243–266. Springer, Heidelberg (1988)
Konikowska, B., Tarlecki, A., Blikle, A.: A Three-valued Logic for Software Specification and Validation. Fundam. Inform. 14(4), 411–453 (1991)
Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. Springer (2012)
Cheng, J.H., Jones, C.B.: On the Usability of Logics which Handle Partial Functions. In: Morgan, C., Woodcock, J.C.P. (eds.) 3rd Refinement Workshop, pp. 51–69 (1991)
Jones, C.B.: Reasoning about Partial Functions in the Formal Development of Programs. Electronic Notes in Theoretical Computer Science 145, 3–25 (2006)
Schreiner, W.: Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs. In: Quaresma, P., Back, R.-J. (eds.) Proceedings First Workshop on CTP Components for Educational Software (THedu 2011), Wrocław, Poland. Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 79, pp. 124–142 (July 31, 2012) ISSN: 2075-2180
Schreiner, W.: A Program Calculus Technical Report. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria (2008), http://www.risc.uni-linz.ac.at/people/schreine/papers/ProgramCalculus2008.pdf
Jones, C.B., Middelburg, C.A.: A Typed Logic of Partial Functions Reconstructed Classically. Acta Informatica 31(5), 399–430 (1994)
Broy, M., Wirsing, M.: Partial Abstract Data Types. Acta Informatica 18(1), 47–64 (1982)
Burmeister, P.: A Model Theoretic Oriented Approach to Partial Algebras. Akademie-Verlag (1986)
Kreowski, H.-J.: Partial Algebra Flows from Algebraic Specifications. 14th Int. Colloquium on Automata, Languages and Programming. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 521–530. Springer, Heidelberg (1987)
Reichel, H.: Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press (1987)
Mosses, P.D. (ed.): CASL Reference Manual: The Complete Documentation of the Common Algebraic Specification Language. LNCS, vol. 2960. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing
About this paper
Cite this paper
Kryvolap, A., Nikitchenko, M., Schreiner, W. (2013). Extending Floyd-Hoare Logic for Partial Pre- and Postconditions. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds) Information and Communication Technologies in Education, Research, and Industrial Applications. ICTERI 2013. Communications in Computer and Information Science, vol 412. Springer, Cham. https://doi.org/10.1007/978-3-319-03998-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-03998-5_18
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03997-8
Online ISBN: 978-3-319-03998-5
eBook Packages: Computer ScienceComputer Science (R0)