<abstract xmlns="http://www.w3.org/1999/xhtml">This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:<preformat preformat-type="transcription">
i := val.1
j := val.2
b := val.3
n := val.4
s := val.5
while (i &lt;> n)
 i := i + j
 s := s * b
return s
</preformat>computing the natural n power of given complex number b, where variables <monospace>i, b, n, s</monospace> are located as values of a <monospace>V-valued Function, loc,</monospace> as: <monospace>loc/.1 = i, loc/.3 = b, loc/.4 = n</monospace> and <monospace>loc/.5 = s,</monospace> and the constant 1 is located in the location <monospace>loc/.2 = j</monospace> (set <monospace>V</monospace> represents simple names of considered nominative data [17]).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 post-conditions [14],[16],[7],[5].</abstract>

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:
i := val.1
j := val.2
b := val.3
n := val.4
s := val.5
while (i <> n)
 i := i + j
 s := s * b
return s
computing the natural n power of given complex number b, where variables i, b, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = b, loc/.4 = n and loc/.5 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [17]).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 post-conditions [14],[16],[7],[5].

Partial Correctness of a Power Algorithm

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Partial Correctness of a Power Algorithm"}

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. In this...

Partial Correctness of a Power Algorithm

Publicado en línea: 20 jul 2019

Páginas: 189 - 195

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0018

Palabras clave
power, nominative data, program verification

© 2019 Adrian Jaszczak, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Partial Correctness of a Power Algorithm

Publicado en línea: 20 jul 2019

Páginas: 189 - 195

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0018

Palabras clavepower, nominative data, program verification

© 2019 Adrian Jaszczak, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Palabras clave
power, nominative data, program verification