Implementation of the composition-nominative approach to program formalization in Mizar

zbMath1390.68183MaRDI QIDQ1650410

Ievgen Ivanov, Artur Korniłowicz, Mykola Nikitchenko

Publication date: 3 July 2018

Published in: Computer Science Journal of Moldova (Search for Journal in Brave)

Full work available at URL: http://www.math.md/publications/csjm/issues/v26-n1/12569/

zbMATH Keywords

formal methodssemistructured dataproof assistantprogram semanticsformalization

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

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 ⋮ Partial correctness of a Fibonacci algorithm

Uses Software

• Mizar

Cites Work

• Kleene algebra of partial predicates
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item