Partial correctness of a factorial algorithm

DOI10.2478/FORMA-2019-0017MaRDI QIDQ2337337zbMATH OpenOpenAlexWikidataFDO

Authors Adrian Jaszczak, Artur Korniłowicz

Publication date 19 November 2019

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-2019-0017

zbMATH Keywords

factorialnominative dataprogram verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Partial correctness of a Fibonacci algorithm
• Partial correctness of GCD algorithm
• Partial correctness of a power algorithm
• An improved computational algorithm for finding the factorial
• On the complexity of calculating factorials
• scientific article; zbMATH DE number 991430
• scientific article; zbMATH DE number 1046599
• scientific article; zbMATH DE number 3926528
• scientific article; zbMATH DE number 1962810

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
• 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

(5)

• Partial correctness of a Fibonacci algorithm
• Partial correctness of GCD algorithm
• Partial correctness of a power algorithm
• General theory and tools for proving algorithms in nominative data systems
• 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 factorial algorithm

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