Advertisement

Inference Rules for the Partial Floyd-Hoare Logic Based on Composition of Predicate Complement

  • Ievgen Ivanov
  • Mykola NikitchenkoEmail author
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1007)

Abstract

Classical Floyd-Hoare logic is sound when total pre- and post-conditions are considered. In the case of partial conditions (predicates) the logic becomes unsound. This situation may be corrected by introducing additional constraints to the rules of the logic. But such constraints, in particular, for the sequence and while rules, are rather complicated. In this paper we propose new simpler rules formulated in a program algebra extended with the composition of predicate complement. The obtained logic is called the Complemented Partial Floyd-Hoare Logic (CPFHL). The predicate component of this logic is related to three-valued logic. We prove the soundness theorem for CPFHL and discuss further investigations of the problem. The obtained results can be useful for software verification.

Keywords

Formal methods Software verification Partial predicate Floyd-Hoare logic 

References

  1. 1.
    Ivanov, I., Nikitchenko, M.: On the sequence rule for the Floyd-Hoare logic with partial pre-and post-conditions. In: CEUR Workshop Proceedings. Proceedings of the 14th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer. Volume II: Workshops, Kyiv, Ukraine, 14–17 May 2018, vol. 2104, pp. 716–724 (2018)Google Scholar
  2. 2.
    Floyd, R.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol. 19, pp. 19–32 (1967)Google Scholar
  3. 3.
    Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefGoogle Scholar
  4. 4.
    Apt, K.: Ten years of Hoare’s logic: a survey - part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefGoogle Scholar
  5. 5.
  6. 6.
  7. 7.
    Jones, C.: Reasoning about partial functions in the formal development of programs. Electron. Notes Theor. Comput. Sci. 145, 3–25 (2006). Proceedings of AVoCS 2005. ElsevierCrossRefGoogle Scholar
  8. 8.
    Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Logic J. IGPL 13(4), 415–433 (2005)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Gries, D., Schneider, F.: Avoiding the undefined by underspecification. Technical report, Ithaca, NY, USA (1995)CrossRefGoogle Scholar
  10. 10.
    Nikitchenko, M., Kryvolap, A.: Properties of inference systems for Floyd-Hoare logic with partial predicates. Acta Electrotechnica et Informatica 13(4), 70–78 (2013)CrossRefGoogle Scholar
  11. 11.
    Kryvolap, A., Nikitchenko, M., Schreiner, W.: Extending Floyd-Hoare logic for partial pre- and postconditions. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2013. CCIS, vol. 412, pp. 355–378. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-03998-5_18CrossRefGoogle Scholar
  12. 12.
    Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the algebra of nominative data in Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Prague, Czech Republic, 3–6 September 2017, pp. 237–244 (2017)Google Scholar
  13. 13.
    Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the nominative algorithmic algebra in Mizar. In: Świątek, J., Borzemski, L., Wilimowska, Z. (eds.) ISAT 2017. AISC, vol. 656, pp. 176–186. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-67229-8_16CrossRefGoogle Scholar
  14. 14.
    Nielson, H., Nielson, F.: Semantics with Applications - a Formal Introduction. Wiley, Hoboken (1992). Wiley professional computingzbMATHGoogle Scholar
  15. 15.
    Nikitchenko, N.S.: A composition nominative approach to program semantics. Technical report, IT-TR 1998–020, Technical University of Denmark (1998)Google Scholar
  16. 16.
    Skobelev, V., Ivanov, I., Nikitchenko, M.: Nominative data with ordered set of names. Comput. Sci. J. Moldova 25, 195–216 (2017)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Ivanov, I.: On representations of abstract systems with partial inputs and outputs. In: Gopal, T.V., Agrawal, M., Li, A., Cooper, S.B. (eds.) TAMC 2014. LNCS, vol. 8402, pp. 104–123. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-06089-7_8CrossRefGoogle Scholar
  18. 18.
    Ivanov, I.: An abstract block formalism for engineering systems. In: Ermolayev, V., et al. (eds.) Proceedings of the 9th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, CEUR Workshop Proceedings, Kherson, Ukraine, 19–22 June 2013, vol. 1000, pp. 448–463. CEUR-WS.org (2013)Google Scholar
  19. 19.
    Skobelev, V., Nikitchenko, M., Ivanov, I.: On algebraic properties of nominative data and functions. In: Ermolayev, V., Mayr, H., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2014. CCIS, vol. 469, pp. 117–138. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-13206-8_6CrossRefGoogle Scholar
  20. 20.
    Nikitchenko, M., Ivanov, I.: Composition-nominative languages of programs with associative denaming. Visnyk (Bull.) Lviv Univ. Ser. Appl. Math. Inform. 16, 124–139 (2010)Google Scholar
  21. 21.
    Nikitchenko, M., Ivanov, I., Skobelev, V.: Proving properties of programs on hierarchical nominative data. Comput. Sci. J. Moldova 24(3(72)), 371–398 (2016)MathSciNetzbMATHGoogle Scholar
  22. 22.
    Kleene, S.: Introduction to Metamathematics. North-Holland Publishing Co. and P. Noordhoff, Amsterdam and Groningen (1952)zbMATHGoogle Scholar
  23. 23.
    Korniłowicz, A., Ivanov, I., Nikitchenko, M.: Kleene algebra of partial predicates. Formalized Math. 26, 11–20 (2018)CrossRefGoogle Scholar
  24. 24.
    Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: An approach to formalization of an extension of Floyd-Hoare logic. In: Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, 15–18 May 2017, pp. 504–523 (2017)Google Scholar
  25. 25.
    Nikitchenko, M., Shkilniak, S.: Semantic properties of T-consequence relation in logics of quasiary predicates. Comput. Sci. J. Moldova 23(2(68)), 102–122 (2015)MathSciNetzbMATHGoogle Scholar
  26. 26.
    Nikitchenko, M., Ivanov, I., Korniłowicz, A., Kryvolap, A.: Extended Floyd-Hoare Logic over relational nominative data. In: Bassiliades, N., et al. (eds.) ICTERI 2017. CCIS, vol. 826, pp. 41–64. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-76168-8_3CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Taras Shevchenko National University of KyivKyivUkraine

Personalised recommendations