Partial Correctness of an Algorithm Computing Lucas Sequences

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 [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...

Full description

Bibliographic Details
Main Author: Jaszczak Adrian
Format: Article
Language:English
Published: Sciendo 2020-12-01
Series:Formalized Mathematics
Subjects:
nominative data
program verification
lucas sequences
68q60
03b70
68v20
Online Access:https://doi.org/10.2478/forma-2020-0025
id doaj-d5a8d8b235794b9bb89a1bea6c0d9449
record_format Article
spelling doaj-d5a8d8b235794b9bb89a1bea6c0d94492021-09-05T21:01:04ZengSciendoFormalized Mathematics1898-99342020-12-0128427928810.2478/forma-2020-0025Partial Correctness of an Algorithm Computing Lucas SequencesJaszczak Adrian0Institute of Informatics, University of Białystok, PolandIn 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].https://doi.org/10.2478/forma-2020-0025nominative dataprogram verificationlucas sequences68q6003b7068v20
collection DOAJ
language English
format Article
sources DOAJ
author Jaszczak Adrian
spellingShingle Jaszczak Adrian
Partial Correctness of an Algorithm Computing Lucas Sequences
Formalized Mathematics
nominative data
program verification
lucas sequences
68q60
03b70
68v20
author_facet Jaszczak Adrian
author_sort Jaszczak Adrian
title Partial Correctness of an Algorithm Computing Lucas Sequences
title_short Partial Correctness of an Algorithm Computing Lucas Sequences
title_full Partial Correctness of an Algorithm Computing Lucas Sequences
title_fullStr Partial Correctness of an Algorithm Computing Lucas Sequences
title_full_unstemmed Partial Correctness of an Algorithm Computing Lucas Sequences
title_sort partial correctness of an algorithm computing lucas sequences
publisher Sciendo
series Formalized Mathematics
issn 1898-9934
publishDate 2020-12-01
description 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].
topic nominative data
program verification
lucas sequences
68q60
03b70
68v20
url https://doi.org/10.2478/forma-2020-0025
work_keys_str_mv AT jaszczakadrian partialcorrectnessofanalgorithmcomputinglucassequences
_version_ 1717781771363287040

Similar Items