Skip to main content
SpringerLink
Log in
Book cover

International Conference on Information and Communication Technologies in Education, Research, and Industrial Applications

ICTERI 2013: Information and Communication Technologies in Education, Research, and Industrial Applications pp 355–378Cite as

Extending Floyd-Hoare Logic for Partial Pre- and Postconditions

  • Conference paper

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 412))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Floyd, R.W.: Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19, 19–31 (1967)

    Article  MathSciNet  Google Scholar 

  2. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM (12), 576–580 (1969)

    Google Scholar 

  3. 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)

    Google Scholar 

  4. Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction, p. 240. John Wiley & Sons Inc. (1992)

    Google Scholar 

  5. Nikitchenko, M.S., Tymofieiev, V.G.: Satisfiability in Composition-Nominative Logics. Central European Journal of Computer Science 2(3), 194–213 (2012)

    Article  Google Scholar 

  6. Avron, A., Zamansky, A.: Non-Deterministic Semantics for Logical Systems. Handbook of Philosophical Logic 16, 227–304 (2011)

    Article  Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  9. Schmidt, D.A.: Denotational Semantics – A Methodology for Language Development. Allyn and Bacon, Boston (1986)

    Google Scholar 

  10. 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)

    Google Scholar 

  11. Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)

    Book  MATH  Google Scholar 

  12. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, London (1998)

    Google Scholar 

  13. 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)

    Article  Google Scholar 

  14. 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)

    Article  MATH  Google Scholar 

  15. Ł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)

    Google Scholar 

  16. Kleene, S.C.: On Notation for Ordinal Numbers. Journal Symbolic Logic 3, 150–155 (1938)

    Article  Google Scholar 

  17. 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)

    Google Scholar 

  18. Bergmann, M.: An Introduction to Many-Valued and Fuzzy Logic: Semantics, Algebras, and Derivation Systems. Cambridge University Press, Cambridge (2008)

    Book  Google Scholar 

  19. Moisil, G.: Recherches sur les logiques nonchrysippiennes. Ann. Sci. Univ. Jassy 26, 431–436 (1940)

    MathSciNet  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Bergstra, J.A., Ponse, A.: Bochvar-McCarthy Logic and Process Algebra. Notre Dame Journal of Formal Logic 39(4), 464–484 (1988)

    MathSciNet  Google Scholar 

  22. 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)

    Google Scholar 

  23. Konikowska, B., Tarlecki, A., Blikle, A.: A Three-valued Logic for Software Specification and Validation. Fundam. Inform. 14(4), 411–453 (1991)

    MathSciNet  MATH  Google Scholar 

  24. Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. Springer (2012)

    Google Scholar 

  25. 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)

    Google Scholar 

  26. Jones, C.B.: Reasoning about Partial Functions in the Formal Development of Programs. Electronic Notes in Theoretical Computer Science 145, 3–25 (2006)

    Google Scholar 

  27. 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

    Google Scholar 

  28. 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

  29. Jones, C.B., Middelburg, C.A.: A Typed Logic of Partial Functions Reconstructed Classically. Acta Informatica 31(5), 399–430 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  30. Broy, M., Wirsing, M.: Partial Abstract Data Types. Acta Informatica 18(1), 47–64 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  31. Burmeister, P.: A Model Theoretic Oriented Approach to Partial Algebras. Akademie-Verlag (1986)

    Google Scholar 

  32. 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)

    Chapter  Google Scholar 

  33. Reichel, H.: Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press (1987)

    Google Scholar 

  34. Mosses, P.D. (ed.): CASL Reference Manual: The Complete Documentation of the Common Algebraic Specification Language. LNCS, vol. 2960. Springer, Heidelberg (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Taras Shevchenko National University of Kyiv, Kyiv, Ukraine

    Andrii Kryvolap & Mykola Nikitchenko

  2. Johannes Kepler University, Linz, Austria

    Wolfgang Schreiner

Authors
  1. Andrii Kryvolap
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mykola Nikitchenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wolfgang Schreiner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information Technologies, Zaporozhye National University, Zhukovskogo st. 66, 69063, Zaporozhye, Ukraine

    Vadim Ermolayev

  2. Mayr Application Engineering, Alpen-Adria University Klagenfurt, Universitätsstrasse 65, 9020, Klagenfurt, Austria

    Heinrich C. Mayr

  3. Department of Theory and Technology of Programming, Taras Shevchenko National University of Kyiv, 64, Volodymyrska Street, 01601, Kyiv, Ukraine

    Mykola Nikitchenko

  4. Kherson State University, Ukraine

    Aleksander Spivakovsky

  5. School of Mathematics and Mechanics, V.N. Karazin Kharkiv National University, 4, Svobody Sqr., 61022, Kharkiv, Ukraine

    Grygoriy Zholtkevych

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation