@MISC{NOMIN_9.MIZ,
  AUTHOR = {Jaszczak, Adrian},
  TITLE = {Partial correctness of an algorithm computing Lucas sequences},
  DAY = {25},
  MONTH = {October},
  YEAR = {2020},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SECTION1 = {Introduction about finite sequences},
  SECTION2 = {Lucas sequences},
  SECTION3 = {Main algorithm},
  SUMMARY = {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 with given $P$ and $Q$ coefficients as well as two first 
  elements ($x$ and $y$). The algorithm is encoded in nominative data 
  language \cite{Skobelev2014} in the Mizar system \cite{FourDecades,BancerekJAR:2018}.
  \begin{verbatim}
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
\end{verbatim}\par
This paper continues verification of algorithms 
\cite{NOMIN_4.ABS,NOMIN_5.ABS,NOMIN_6.ABS,NOMIN_7.ABS,NOMIN_8.ABS} written 
in terms of simple-named complex-valued nominative 
data \cite{NOMIN_1.ABS,NOMIN_2.ABS,PARTPR_1.ABS,PARTPR_2.ABS,
DBLP:conf/fedcsis/KornilowiczKNI17,DBLP:conf/isat/KornilowiczKNI17}.
The validity of the algorithm is presented in terms of semantic 
Floyd-Hoare triples over such data \cite{NOMIN_3.ABS}.
Proofs of the correctness are based on an~inference system for 
an~extended Floyd-Hoare logic \cite{Floyd1967,Hoare1969} with partial 
pre- and post-conditions \cite{KornilowiczetalICTERI2017,
Kryvolap2013,Moldova2018,SeqRule2018}.},}
