REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/8135
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorJaszczak, Adrian-
dc.contributor.authorKorniłowicz, Artur-
dc.date.accessioned2019-07-29T08:28:50Z-
dc.date.available2019-07-29T08:28:50Z-
dc.date.issued2019-
dc.identifier.citationFormalized Mathematics, Volume 27, Issue 2, Pages 181 - 187-
dc.identifier.issn1426-2630-
dc.identifier.urihttp://hdl.handle.net/11320/8135-
dc.description.abstractIn this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm: i := val.1 j := val.2 n := val.3 s := val.4 while (i <> n) i := i + j s := s * i return s computing the factorial of given natural number n, where variables i, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = n and loc/.4 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [16]).This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [13],[15],[7],[5].-
dc.language.isoen-
dc.publisherDeGruyter Open-
dc.subjectfactorial-
dc.subjectnominative data-
dc.subjectprogram verification-
dc.subject68Q60-
dc.subject68T37-
dc.subject03B70-
dc.subject03B35-
dc.titlePartial Correctness of a Factorial Algorithm-
dc.typeArticle-
dc.identifier.doi10.2478/forma-2019-0017-
dc.description.AffiliationAdrian Jaszczak - Institute of Informatics, University of Białystok, Poland-
dc.description.AffiliationArtur Korniłowicz - Institute of Informatics, University of Białystok, Poland-
dc.description.referencesGrzegorz 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.-
dc.description.referencesR.W. Floyd. Assigning meanings to programs. Mathematical aspects of computer science, 19(19–32), 1967.-
dc.description.referencesAdam 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.-
dc.description.referencesC.A.R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10): 576–580, 1969.-
dc.description.referencesIevgen 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.-
dc.description.referencesIevgen 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.-
dc.description.referencesIevgen 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.-
dc.description.referencesIevgen 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.-
dc.description.referencesIevgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized Mathematics, 26(2): 159–164, 2018. doi:10.2478/forma-2018-0013.-
dc.description.referencesIevgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On algebras of algorithms and specifications over uninterpreted data. Formalized Mathematics, 26(2):141–147, 2018. doi:10.2478/forma-2018-0011.-
dc.description.referencesArtur Kornilowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. Formalization of the algebra of nominative data in Mizar. In Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Prague, Czech Republic, September 3–6, 2017., pages 237–244, 2017. ISBN 978-83-946253-7-5. doi:10.15439/2017F301.-
dc.description.referencesArtur Kornilowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. Formalization of the nominative algorithmic algebra in Mizar. In Leszek Borzemski, Jerzy Świątek, and Zofia Wilimowska, editors, Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology – ISAT 2017 – Part II, Szklarska Poręba, Poland, September 17–19, 2017, volume 656 of Advances in Intelligent Systems and Computing, pages 176–186. Springer, 2017. ISBN 978-3-319-67228-1. doi:10.1007/978-3-319-67229-8_16.-
dc.description.referencesArtur 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.-
dc.description.referencesArtur 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.-
dc.description.referencesAndrii 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.-
dc.description.referencesVolodymyr G. Skobelev, Mykola Nikitchenko, and Ievgen Ivanov. On algebraic properties of nominative data and functions. In Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, and Grygoriy Zholtkevych, editors, Information and Communication Technologies in Education, Research, and Industrial Applications – 10th International Conference, ICTERI 2014, Kherson, Ukraine, June 9–12, 2014, Revised Selected Papers, volume 469 of Communications in Computer and Information Science, pages 117–138. Springer, 2014. ISBN 978-3-319-13205-1. doi:10.1007/978-3-319-13206-8_6.-
dc.identifier.eissn1898-9934-
dc.description.volume27-
dc.description.issue2-
dc.description.firstpage181-
dc.description.lastpage187-
dc.identifier.citation2Formalized Mathematics-
dc.identifier.orcid0000-0003-4899-4983-
dc.identifier.orcid0000-0002-4565-9082-
Występuje w kolekcji(ach):Artykuły naukowe (WInf)
Formalized Mathematics, 2019, Volume 27, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2019_27_2_008.pdf231,91 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons