Partial correctness of a Fibonacci algorithm

DOI10.2478/FORMA-2020-0016MaRDI QIDQ2113835zbMATH OpenOpenAlexFDO

Authors Artur Korniłowicz

Publication date 14 March 2022

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

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

zbMATH Keywords

Fibonacci sequencenominative dataprogram verification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Partial correctness of an algorithm computing Lucas sequences
• Partial correctness of a factorial algorithm
• Partial correctness of a power algorithm
• General theory and tools for proving algorithms in nominative data systems
• Partial correctness of GCD algorithm

Cites work

• An axiomatic basis for computer programming
• An inference system of an extension of Floyd-Hoare logic for partial predicates
• Four decades of \textsc{Mizar}. Foreword
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Implementation of the composition-nominative approach to program formalization in Mizar
• 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
• Partial correctness of a factorial algorithm
• Partial correctness of a power algorithm
• Partial correctness of GCD algorithm
• Proving properties of programs on hierarchical nominative data
• Simple-named complex-valued nominative data -- definition and basic operations
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(2)

• Partial correctness of a factorial algorithm
• Partial correctness of an algorithm computing Lucas sequences

Describes a project that uses

Uses Software

• Mizar

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2113835)