Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/10835
Tytuł: | Partial Correctness of a Fibonacci Algorithm |
Autorzy: | Korniłowicz, Artur |
Słowa kluczowe: | nominative data program verification Fibonacci sequence |
Data wydania: | 2020 |
Data dodania: | 4-maj-2021 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 28, Issue 2, Pages 187-196 |
Abstrakt: | In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language [19] in the Mizar system [3], [1]. It is tested on verification of the partial correctness of an algorithm computing n-th Fibonacci number: i := 0 s := 0 b := 1 c := 0 while (i <> n) c := s s := b b := c + s i := i + 1 return s This paper continues verification of algorithms [10], [13], [12] written in terms of simple-named complex-valued nominative data [6], [8], [17], [11], [14], [15]. 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 [16], [18], [7], [5]. |
Afiliacja: | Institute of Informatics, University of Białystok, Poland |
URI: | http://hdl.handle.net/11320/10835 |
DOI: | 10.2478/forma-2020-0016 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0002-4565-9082 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2020 University of Białymstoku; CC-BY-SA License ver. 3.0 or later; |
Występuje w kolekcji(ach): | Artykuły naukowe (WInf) Formalized Mathematics, 2020, Volume 28, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2020-0016.pdf | 277,12 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL