@MISC{NOMIN_7.MIZ,
  AUTHOR = {Korni{\l}owicz, Artur},
  TITLE = {Partial Correctness of a Fibonacci Algorithm},
  DAY = {31},
  MONTH = {May},
  YEAR = {2020},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SECTION1 = {Introduction},
  SECTION2 = {Main algorithm},
  SUMMARY = {In this paper we introduce some notions to facilitate formulating and 
  proving properties of iterative algorithms encoded in nominative data language 
  \cite{Skobelev2014} in the Mizar system \cite{FourDecades,BancerekJAR:2018}.
  It is tested on verification of the partial correctness of an algorithm 
  computing $n$-th Fibonacci number:
  \begin{verbatim}
i := 0
s := 0
b := 1
c := 0
while ( i <> n )
  c := s
  s := b
  b := c + s
  i := i + 1
return s
  \end{verbatim}\par
  This paper continues verification of algorithms 
  \cite{NOMIN_4.ABS,NOMIN_5.ABS,NOMIN_6.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}.},}
