An inference system of an extension of Floyd-Hoare logic for partial predicates

DOI10.2478/forma-2018-0013zbMath1422.03059OpenAlexW2907861474WikidataQ128657926 ScholiaQ128657926MaRDI QIDQ2311523

Ievgen Ivanov, Artur Korniłowicz, Mykola Nikitchenko

Publication date: 10 July 2019

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2018-0013

zbMATH Keywords

inference ruleprogram verificationFloyd-Hoare logicFloyd-Hoare triple

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Logic programming (68N17)

Related Items

Partial correctness of a factorial algorithm, Partial correctness of a power algorithm, Partial correctness of a Fibonacci algorithm

Uses Software

• Mizar

Cites Work

• Four decades of {\textsc{Mizar}}. Foreword
• Implementation of the composition-nominative approach to program formalization in Mizar
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Simple-named complex-valued nominative data -- definition and basic operations
• Kleene algebra of partial predicates