Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/8136
Tytuł: | Partial Correctness of a Power Algorithm |
Autorzy: | Jaszczak, Adrian |
Słowa kluczowe: | power nominative data program verification 68Q60 68T37 03B70 03B35 |
Data wydania: | 2019 |
Data dodania: | 29-lip-2019 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 27, Issue 2, Pages 189 - 195 |
Abstrakt: | This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. 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 b := val.3 n := val.4 s := val.5 while (i <> n) i := i + j s := s * b return s computing the natural n power of given complex number b, where variables i, b, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = b, loc/.4 = n and loc/.5 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [17]).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 [14],[16],[7],[5]. |
Afiliacja: | Institute of Informatics, University of Białystok, Poland |
URI: | http://hdl.handle.net/11320/8136 |
DOI: | 10.2478/forma-2019-0018 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0003-4899-4983 |
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 | Rozmiar | Format | |
---|---|---|---|---|
forma_2019_27_2_009.pdf | 232,25 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL