@MISC{NOMIN_8.MIZ,
AUTHOR = {Jaszczak, Adrian},
TITLE = {General theory and tools for proving algorithms in nominative data systems},
  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},
SUMMARY = {In this paper we introduce some new definitions for sequences of 
  operations and extract general theorems about properties of iterative algorithms
  encoded in nominative data language \cite{Skobelev2014} in the 
  Mizar system \cite{FourDecades,BancerekJAR:2018} in order to simplify the 
  process of proving algorithms in the future.\par
  This paper continues verification 
  of algorithms \cite{NOMIN_4.ABS,NOMIN_5.ABS,NOMIN_6.ABS,NOMIN_7.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}.\par
  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}.},}
