REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

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].
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 (WMiI)
Formalized Mathematics, 2018, Volume 26, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2018_26_2_006.pdf222,9 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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