<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

Publicado en línea: 21 may 2021

Páginas: 269 - 278

Aceptado: 25 oct 2020

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

Palabras clave
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

Publicado en línea: 21 may 2021

Páginas: 269 - 278

Aceptado: 25 oct 2020

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

Palabras clavenominative 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.

Palabras clave
nominative data, program verification, inference rules