An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates

In the paper we give a formalization in the Mizar system [2, 1] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions which was proposed in [7, 9]. The rules are formalized on the semantic level. The details of the approach used to implement this formalization are described in [5].We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) [5] which is a triple of a pre-condition represented by a partial predicate, a program, represented by a partial function which maps data to data, and a post-condition, represented by a partial predicate, which informally means that if the pre-condition on a program’s input data is defined and true, and the program’s output after a run on this data is defined (a program terminates successfully), and the post-condition is defined on the program’s output, then the post-condition is true.We formalize and prove the soundness of the rules of the inference system [9, 7] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in [3].The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data [4]. Application of these rules often requires reasoning about partial predicates representing preand post-conditions which can be done using the formalized results on the Kleene algebra of partial predicates given in [8].Ievgen Ivanov - Taras Shevchenko National University, Kyiv, UkraineArtur Korniłowicz - Institute of Informatics, University of Białystok, PolandMykola Nikitchenko - Taras Shevchenko National University, Kyiv, UkraineGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.Ievgen Ivanov and Mykola Nikitchenko. On the sequence rule for the Floyd-Hoare logic with partial pre- and post-conditions. In Proceedings of the 14th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer. Volume II: Workshops, Kyiv, Ukraine, May 14–17, 2018, volume 2104 of CEUR Workshop Proceedings, pages 716–724, 2018.Ievgen Ivanov, Mykola Nikitchenko, Andrii Kryvolap, and Artur Korniłowicz. Simple-named complex-valued nominative data – definition and basic operations. Formalized Mathematics, 25(3):205–216, 2017. doi:10.1515/forma-2017-0020.Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. Implementation of the composition-nominative approach to program formalization in Mizar. The Computer Science Journal of Moldova, 26(1):59–76, 2018.Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On an algorithmic algebra over simple-named complex-valued nominative data. Formalized Mathematics, 26(2):149–158, 2018. doi:10.2478/forma-2018-0012.Artur Korniłowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. An approach to formalization of an extension of Floyd-Hoare logic. In Vadim Ermolayev, Nick Bassiliades, Hans-Georg Fill, Vitaliy Yakovyna, Heinrich C. Mayr, Vyacheslav Kharchenko, Vladimir Peschanenko, Mariya Shyshkina, Mykola Nikitchenko, and Aleksander Spivakovsky, editors, Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, May 15–18, 2017, volume 1844 of CEUR Workshop Proceedings, pages 504–523. CEUR-WS.org, 2017.Artur Korniłowicz, Ievgen Ivanov, and Mykola Nikitchenko. Kleene algebra of partial predicates. Formalized Mathematics, 26(1):11–20, 2018. doi:10.2478/forma-2018-0002.Andrii Kryvolap, Mykola Nikitchenko, and Wolfgang Schreiner. Extending Floyd-Hoare logic for partial pre- and postconditions. In Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, and Grygoriy Zholtkevych, editors, Information and Communication Technologies in Education, Research, and Industrial Applications: 9th International Conference, ICTERI 2013, Kherson, Ukraine, June 19–22, 2013, Revised Selected Papers, pages 355–378. Springer International Publishing, 2013. ISBN 978-3-319-03998-5. doi:10.1007/978-3-319-03998-5_18.26215916