<abstract xmlns="http://www.w3.org/1999/xhtml">

In this paper we introduce some new definitions for sequences of operations and extract general theorems about properties of iterative algorithms encoded in nominative data language [20] in the Mizar system [3], [1] in order to simplify the process of proving algorithms in the future.
This paper continues verification of algorithms [10], [13], [12], [14] written in terms of simple-named complex-valued nominative data [6], [8], [18], [11], [15], [16].
The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2], [4] with partial pre- and postconditions [17], [19], [7], [5].
</abstract>

In this paper we introduce some new definitions for sequences of operations and extract general theorems about properties of iterative algorithms encoded in nominative data language [20] in the Mizar system [3], [1] in order to simplify the process of proving algorithms in the future.
This paper continues verification of algorithms [10], [13], [12], [14] written in terms of simple-named complex-valued nominative data [6], [8], [18], [11], [15], [16].
The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2], [4] with partial pre- and postconditions [17], [19], [7], [5].

General Theory and Tools for Proving Algorithms in Nominative Data Systems

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"General Theory and Tools for Proving Algorithms in Nominative Data Systems"}

In this paper we introduce some new definitions for sequences of operations and extract general theorems about properties of iterative algorithms encoded in...

General Theory and Tools for Proving Algorithms in Nominative Data Systems

Published Online: May 21, 2021

Page range: 269 - 278

Accepted: Oct 25, 2020

DOI: https://doi.org/10.2478/forma-2020-0024

Keywords
nominative data, program verification, inference rules

© 2021 Adrian Jaszczak, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

General Theory and Tools for Proving Algorithms in Nominative Data Systems

Published Online: May 21, 2021

Page range: 269 - 278

Accepted: Oct 25, 2020

DOI: https://doi.org/10.2478/forma-2020-0024

Keywordsnominative data, program verification, inference rules

© 2021 Adrian Jaszczak, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Keywords
nominative data, program verification, inference rules