Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/7625
Tytuł: | An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates |
Autorzy: | Ivanov, Ievgen Korniłowicz, Artur Nikitchenko, Mykola |
Słowa kluczowe: | Floyd-Hoare logic Floyd-Hoare triple inference rule program verification |
Data wydania: | 2018 |
Data dodania: | 4-mar-2019 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 26, Issue 2, Pages 159-164 |
Abstrakt: | In the paper we give a formalization in the Mizar system [2, 1] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions which was proposed in [7, 9]. The rules are formalized on the semantic level. The details of the approach used to implement this formalization are described in [5].We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) [5] which is a triple of a pre-condition represented by a partial predicate, a program, represented by a partial function which maps data to data, and a post-condition, represented by a partial predicate, which informally means that if the pre-condition on a program’s input data is defined and true, and the program’s output after a run on this data is defined (a program terminates successfully), and the post-condition is defined on the program’s output, then the post-condition is true.We formalize and prove the soundness of the rules of the inference system [9, 7] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in [3].The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data [4]. Application of these rules often requires reasoning about partial predicates representing preand post-conditions which can be done using the formalized results on the Kleene algebra of partial predicates given in [8]. |
Afiliacja: | Ievgen Ivanov - Taras Shevchenko National University, Kyiv, Ukraine Artur Korniłowicz - Institute of Informatics, University of Białystok, Poland Mykola Nikitchenko - Taras Shevchenko National University, Kyiv, Ukraine |
URI: | http://hdl.handle.net/11320/7625 |
DOI: | 10.2478/forma-2018-0013 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | brakorcid 0000-0002-4565-9082 0000-0002-4078-1062 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Artykuły naukowe (WInf) Formalized Mathematics, 2018, Volume 26, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2018_26_2_006.pdf | 222,9 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL