Top

Published in:

2018 | OriginalPaper | Chapter

Extended Floyd-Hoare Logic over Relational Nominative Data

Authors : Mykola Nikitchenko, Ievgen Ivanov, Artur Korniłowicz, Andrii Kryvolap

Published in: Information and Communication Technologies in Education, Research, and Industrial Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The classical Floyd-Hoare logic is defined for the case of total pre- and postconditions and partial programs (i.e. programs can be undefined on some input data, but conditions must be defined on all data). In this paper we propose an extension of this logic for the case of partial conditions and partial programs over structured data. These data are based on two constructing primitives: naming and relational structuring and are called relational nominative data. They can conveniently represent many data structures used in programming. The semantics of the proposed logic is represented by special algebras of partial functions and predicates over relational nominative data. Operations of these algebras are called compositions. We present an inference system for the mentioned logic and propose an approach to its formalization in Mizar proof assistant. The obtained results can be used in software verification.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Two Approaches to Modelling Logical Time in Cyber-Physical Systems

next chapter Rankings of Students Based on Experts’ Assessment and Levels of the Likelihood of Learning Outcome Acquirement

Research on using specialized external systems to increase computational power of the Mizar system is also conducted [19‐21].

Due to the size, the MML is a subject of research on optimization of theorems and definitions [33]. It includes the improvement of legibility of proofs [34‐36] and removing duplications.

Floyd, R.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19–32 (1967)MathSciNetCrossRefMATH

Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefMATH

Apt, K.: Ten years of Hoare’s logic: a survey - part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981). http://doi.acm.org/10.1145/357146.357150 CrossRefMATH

Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Log. J. IGPL 13(4), 415–433 (2005). http://dx.doi.org/10.1093/jigpal/jzi032 MathSciNetCrossRefMATH

Jones, C.: Reasoning about partial functions in the formal development of programs. In: AVoCS 2005. Electronic Notes in Theoretical Computer Science, vol. 145, pp. 3–25. Elsevier (2006). https://doi.org/10.1016/j.entcs.2005.10.002

Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 366–373. Springer, Heidelberg (1995). https://doi.org/10.1007/BFb0015254 CrossRef

Duzi, M.: Do we have to deal with partiality? Misc. Log. 5, 45–76 (2003)

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_18

Nikitchenko, M., Kryvolap, A.: Properties of inference systems for Floyd-Hoare logic with partial predicates. Acta Electrotech. Inform. 13(4), 70–78 (2013)CrossRef

10.

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.) Communications in Computer and Information Science, ICTERI, vol. 469, pp. 117–138. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13206-8_6

11.

Nikitchenko, M., Shkilniak, S.: Mathematical logic and theory of algorithms. Publishing house of Taras Shevchenko National University of Kyiv, Ukraine (2008). (in Ukrainian)

12.

Nikitchenko, M.: Composition-nominative aspects of address programming. Cybern. Syst. Anal. 45, 864 (2009). https://doi.org/10.1007/s10559-009-9159-4 MathSciNetCrossRefMATH

13.

Wiedijk, F. (ed.): The Seventeen Provers of the World. Foreword by Dana S. Scott. LNAI, vol. 3600. Springer, Heidelberg (2006). https://doi.org/10.1007/11542384 MATH

14.

Gordon, M.: Mechanizing programming logics in higher order logic. In: Birtwistle, G., Subrahmanyam, P. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387–439. Springer, New York (1989). https://doi.org/10.1007/978-1-4612-3658-0_10 CrossRef

15.

Von Wright, J., Hekanaho, J., Luostarinen, P., Langbacka, T.: Mechanizing some advanced refinement concepts. Form. Methods Syst. Des. 3(1), 49–81 (1993). https://doi.org/10.1007/BF01383984 CrossRefMATH

16.

Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pa̧k, K., Urban, J.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261–279. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_17 CrossRef

17.

Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191–198 (2015). http://dx.doi.org/10.1007/s10817-015-9345-1 MathSciNetCrossRefMATH

18.

Trybulec, A.: Tarski Grothendieck set theory. Formaliz. Math. 1(1), 9–11 (1990)

19.

Naumowicz, A.: Interfacing external CA systems for Gröbner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010). http://dx.doi.org/10.1080/00207160701864459 CrossRefMATH

20.

Naumowicz, A.: SAT-enhanced Mizar proof checking. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 449–452. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_37 CrossRef

21.

Naumowicz, A.: Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver. J. Autom. Reason. 55(3), 285–294 (2015). http://dx.doi.org/10.1007/s10817-015-9332-6 MathSciNetCrossRefMATH

22.

Korniłowicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203–210 (2013). http://dx.doi.org/10.1007/s10817-012-9261-6 MathSciNetCrossRefMATH

23.

Korniłowicz, A.: Flexary connectives in Mizar. Comput. Lang. Syst. Struct. 44, 238–250 (2015). http://dx.doi.org/10.1016/j.cl.2015.07.002

24.

Korniłowicz, A.: Definitional expansions in Mizar. J. Autom. Reason. 55(3), 257–268 (2015). http://dx.doi.org/10.1007/s10817-015-9331-7 MathSciNetCrossRefMATH

25.

Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27, 356–364 (1980). http://doi.acm.org/10.1145/322186.322198 MathSciNetCrossRefMATH

26.

Grabowski, A., Korniłowicz, A., Schwarzweller, C.: Equality in computer proof-assistants. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2015 FedCSIS. Annals of Computer Science and Information Systems, vol. 5, pp. 45–54. IEEE (2015). https://doi.org/10.15439/2015F229

27.

Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 290–301. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27818-4_21 CrossRef

28.

Korniłowicz, A.: Enhancement of Mizar texts with transitivity property of predicates. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 157–162. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_12 CrossRef

29.

Naumowicz, A., Korniłowicz, A.: Introducing Euclidean relations to Mizar. [47], pp. 245–248. https://doi.org/10.15439/2017F368

30.

Grabowski, A.: Mechanizing complemented lattices within Mizar type system. J. Autom. Reason. 55(3), 211–221 (2015). http://dx.doi.org/10.1007/s10817-015-9333-5 MathSciNetCrossRefMATH

31.

Grabowski, A., Korniłowicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2016 FedCSIS. Annals of Computer Science and Information Systems, vol. 8, pp. 363–371. IEEE (2016). https://doi.org/10.15439/2016F520

32.

Grabowski, A., Jastrzębska, M.: Rough set theory from a math-assistant perspective. In: Kryszkiewicz, M., Peters, J.F., Rybinski, H., Skowron, A. (eds.) RSEISP 2007. LNCS (LNAI), vol. 4585, pp. 152–161. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73451-2_17 CrossRef

33.

Grabowski, A., Schwarzweller, C.: On duplication in mathematical repositories. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) CICM 2010. LNCS (LNAI), vol. 6167, pp. 300–314. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14128-7_26 CrossRef

34.

Pąk, K.: Improving legibility of natural deduction proofs is not trivial. Log. Methods Comput. Sci. 10(3), 1–30 (2014). http://dx.doi.org/10.2168/LMCS-10(3:23)2014 MathSciNet

35.

Pąk, K.: Automated improving of proof legibility in the Mizar system. [48], pp. 373–387. https://doi.org/10.1007/978-3-319-08434-3_27

36.

Pąk, K.: Improving legibility of formal proofs based on the close reference principle is NP-hard. J. Autom. Reason. 55(3), 295–306 (2015). http://dx.doi.org/10.1007/s10817-015-9337-1 MathSciNetCrossRefMATH

37.

Nielson, H., Nielson, F.: Semantics with Applications - A Formal Introduction. Wiley, Hoboken (1992)MATH

38.

Nikitchenko, M., Tymofieiev, V.: Satisfiability in composition-nominative logics. Cent. Eur. J. Comput. Sci. 2(3), 194–213 (2012). https://doi.org/10.2478/s13537-012-0027-3 MATH

39.

Dijkstra, E.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1997)MATH

40.

Nikitchenko, M., Shkilniak, S.: Semantic properties of T-consequence relation in logics of quasiary predicates. Comput. Sci. J. Mold. 23(2(68)), 102–122 (2015)MathSciNet

41.

Ivanov, I., Korniłowicz, A., Nikitchenko, M.: Formalization of nominative data in Mizar. In: Proceedings of TAAPSD 2015, pp. 82–85. Taras Shevchenko National University of Kyiv, Ukraine, 23–26 December 2015

42.

Ivanov, I., Nikitchenko, M., Kryvolap, A., Korniłowicz, A.: Simple-named complex-valued nominative data - definition and basic operations. Formaliz. Math. 25(3), 205–216 (2017). http://dx.doi.org/10.1515/forma-2017-0020 CrossRefMATH

43.

Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the algebra of nominative data in Mizar. [47], pp. 237–244. https://doi.org/10.15439/2017F301

44.

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_16

45.

Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge (2000)MATH

46.

Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th LICS, pp. 55–74 (2002)

47.

Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.): Proceedings of FedCSIS 2017. Annals of Computer Science and Information Systems, vol. 11. IEEE, Prague, Czech Republic, 3–6 September 2017

48.

Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.): CICM 2014. LNCS (LNAI), vol. 8543. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3

Title: Extended Floyd-Hoare Logic over Relational Nominative Data
Authors: Mykola Nikitchenko
Ievgen Ivanov
Artur Korniłowicz
Andrii Kryvolap
Publisher: Springer International Publishing
Book: Information and Communication Technologies in Education, Research, and Industrial Applications
Print ISBN: 978-3-319-76167-1

Electronic ISBN: 978-3-319-76168-8

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-76168-8_3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner