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

In this paper we define some properties about finite sequences and verify the partial correctness of an algorithm computing <italic>n</italic>-th element of Lucas sequence [23], [20] with given <italic>P</italic> and <italic>Q</italic> coefficients as well as two first elements (<italic>x</italic> and <italic>y</italic>). The algorithm is encoded in nominative data language [22] in the Mizar system [3], [1].
<disp-quote><monospace>i := 0</monospace>
<monospace>s := x</monospace>
<monospace>b := y</monospace>
<monospace>c := x</monospace>
<monospace>while (i &lt;> n)</monospace>
 <monospace>c := s</monospace>
 <monospace>s := b</monospace>
 <monospace>ps := p*s</monospace>
 <monospace>qc := q*c</monospace>
 <monospace>b := ps − qc</monospace>
 <monospace>i := i + j</monospace>
<monospace>return s</monospace></disp-quote>
This paper continues verification of algorithms [10], [14], [12], [15], [13] written in terms of simple-named complex-valued nominative data [6], [8], [19], [11], [16], [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 [18], [21], [7], [5].
</abstract>

In this paper we define some properties about finite sequences and verify the partial correctness of an algorithm computing n-th element of Lucas sequence [23], [20] with given P and Q coefficients as well as two first elements (x and y). The algorithm is encoded in nominative data language [22] in the Mizar system [3], [1].
i := 0
s := x
b := y
c := x
while (i <> n)
 c := s
 s := b
 ps := p*s
 qc := q*c
 b := ps − qc
 i := i + j
return s
This paper continues verification of algorithms [10], [14], [12], [15], [13] written in terms of simple-named complex-valued nominative data [6], [8], [19], [11], [16], [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 [18], [21], [7], [5].

Partial Correctness of an Algorithm Computing Lucas Sequences

Formalized Mathematics

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

{"article-title":"Partial Correctness of an Algorithm Computing Lucas Sequences"}

In this paper we define some properties about finite sequences and verify the partial correctness of an algorithm computing n-th element of Lucas sequence...

Partial Correctness of an Algorithm Computing Lucas Sequences

Publicado en línea: 21 may 2021

Páginas: 279 - 288

Aceptado: 25 oct 2020

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

Palabras clave
nominative data, program verification, Lucas sequences

© 2021 Adrian Jaszczak, published by Sciendo

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

Partial Correctness of an Algorithm Computing Lucas Sequences

Publicado en línea: 21 may 2021

Páginas: 279 - 288

Aceptado: 25 oct 2020

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

Palabras clavenominative data, program verification, Lucas sequences

© 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, Lucas sequences