<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

Publié en ligne: 21 mai 2021

Pages: 269 - 278

Accepté: 25 oct. 2020

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

Mots clés
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

Publié en ligne: 21 mai 2021

Pages: 269 - 278

Accepté: 25 oct. 2020

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

Mots clésnominative 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.

Mots clés
nominative data, program verification, inference rules