Partial correctness of a Fibonacci algorithm

DOI10.2478/forma-2020-0016OpenAlexW3143907783MaRDI QIDQ2113835

Artur Korniłowicz

Publication date: 14 March 2022

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

Full work available at URL: https://doi.org/10.2478/forma-2020-0016

zbMATH Keywords

Fibonacci sequenceprogram verificationnominative data

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) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Mizar

Cites Work

• Unnamed Item
• Four decades of {\textsc{Mizar}}. Foreword
• Proving properties of programs on hierarchical nominative data
• 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
• On algebras of algorithms and specifications over uninterpreted data
• On an algorithmic algebra over simple-named complex-valued nominative data
• An inference system of an extension of Floyd-Hoare logic for partial predicates
• Partial correctness of GCD algorithm
• Partial correctness of a factorial algorithm
• Partial correctness of a power algorithm
• An axiomatic basis for computer programming

This page was built for publication: Partial correctness of a Fibonacci algorithm