Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/10980
Tytuł: | General Theory and Tools for Proving Algorithms in Nominative Data Systems |
Autorzy: | Jaszczak, Adrian |
Słowa kluczowe: | nominative data program verification inference rules |
Data wydania: | 2020 |
Data dodania: | 24-maj-2021 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 28, Issue 4, Pages 269-278 |
Abstrakt: | In this paper we introduce some new definitions for sequences of operations and extract general theorems about properties of iterative algorithms encoded in nominative data language [20] in the Mizar system [3], [1] in order to simplify the process of proving algorithms in the future. This paper continues verification of algorithms [10], [13], [12], [14] written in terms of simple-named complex-valued nominative data [6], [8], [18], [11], [15], [16]. 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 postconditions [17], [19], [7], [5]. |
Afiliacja: | Institute of Informatics, University of Białystok, Poland |
URI: | http://hdl.handle.net/11320/10980 |
DOI: | 10.2478/forma-2020-0024 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0003-4899-4983 |
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 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2020-0024.pdf | 284,43 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL