REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

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 RozmiarFormat 
10.2478_forma-2020-0016.pdf277,12 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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