REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/8135`
 Tytuł: Partial Correctness of a Factorial Algorithm Autorzy: Jaszczak, AdrianKorniłowicz, Artur Słowa kluczowe: factorialnominative dataprogram verification68Q6068T3703B7003B35 Data wydania: 2019 Data dodania: 29-lip-2019 Wydawca: DeGruyter Open Źródło: Formalized Mathematics, Volume 27, Issue 2, Pages 181 - 187 Abstrakt: In 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]. Afiliacja: Adrian Jaszczak - Institute of Informatics, University of Białystok, PolandArtur Korniłowicz - Institute of Informatics, University of Białystok, Poland URI: http://hdl.handle.net/11320/8135 DOI: 10.2478/forma-2019-0017 ISSN: 1426-2630 e-ISSN: 1898-9934 metadata.dc.identifier.orcid: 0000-0003-4899-49830000-0002-4565-9082 Typ Dokumentu: Article Występuje w kolekcji(ach): Artykuły naukowe (WInf)Formalized Mathematics, 2019, Volume 27, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat