<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

Pubblicato online: 21 mag 2021

Pagine: 269 - 278

Accettato: 25 ott 2020

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

Parole chiave
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

Pubblicato online: 21 mag 2021

Pagine: 269 - 278

Accettato: 25 ott 2020

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

Parole chiavenominative 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.

Parole chiave
nominative data, program verification, inference rules