REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/7626
Tytuł: Partial Correctness of GCD Algorithm
Autorzy: Ivanov, Ievgen
Korniłowicz, Artur
Nikitchenko, Mykola
Słowa kluczowe: greatest common divisor
nominative data
program verification
Data wydania: 2018
Data dodania: 4-mar-2019
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 26, Issue 2, Pages 165-173
Abstrakt: In this paper we present a formalization in the Mizar system [2, 1] of the correctness of the subtraction-based version of Euclid’s algorithm computing the greatest common divisor of natural numbers. The algorithm is written in terms of simple-named complex-valued nominative data [11, 4].The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [7]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions [8, 10, 5, 3].
Afiliacja: Ievgen Ivanov - Taras Shevchenko National University, Kyiv, Ukraine
Artur Korniłowicz - Institute of Informatics, University of Białystok, Poland
Mykola Nikitchenko - Taras Shevchenko National University, Kyiv, Ukraine
URI: http://hdl.handle.net/11320/7626
DOI: 10.2478/forma-2018-0014
ISSN: 1426-2630
e-ISSN: 1898-9934
metadata.dc.identifier.orcid: brakorcid
0000-0002-4565-9082
0000-0002-4078-1062
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2018, Volume 26, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2018_26_2_007.pdf230,29 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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