\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 20. feladat}
\begin{document}
\noindent
\emph{Feladat:} Az azonos értelmezési tartományú $x$ és $y$ vektorop egy p jegyű
($p=x.dom$) decimális szám számjegyeit tartalmazzák (A kisebb indexeken vannak 10 magasabb
hatványainak együtthatói).  Képezzük a $z$ vektorban a számok összegét, és állapítsuk meg,
hogy keletkezett-e túlcsordulás!

\emph{Specifikáció:}\\
$\V = \vect(\Z, \{0, 1, \cdots, 9\})$\\
$A = \alatt{\V}{x} \times \alatt{\V}{y} \times \alatt{\V}{z} \times \alatt{\Z}{k} \times \alatt{\L}{o} \times \alatt{\N_0}{s}$\\
$B = \alatt{\V}{x'} \times \alatt{\V}{y'}$\\
$Q = (x=x' \es y=y' \es x.dom=y.dom=z.dom \es x.hib=y.hib=z.hib)$\\
$R = \left( Q \es \sum\limits_{i\in[x.lob..x.hib]} 10^{x.hib-i}(x[i]+y[i])=10^{x.dom}*\chi(o) +
  \sum\limits_{i\in[x.lob..x.hib]}10^{x.hib-i}z[i] \right)$

\emph{Megoldás:}\\
Most keressük meg a specifikációnak megfelelő megoldó programot! A megoldást
úgy sejtjük, hogy egy ciklussal találhatjuk meg.  Nos, mi legyen ennek a
ciklusnak az invariánsa?

$P = \left( Q \es k\in[x.lob..x.hib+1] \es \sum\limits_{i\in[k..x.hib]} 10^{x.hib-i}(x[i]+y[i])=10^{x.hib-k+1}*\chi(o) +
  \sum\limits_{i\in[k..x.hib]}10^{x.hib-i}z[i] \right)$


Ellenőrízzük le a ciklus feltételeit:\\
\cklegy \\
Jól láthatóan nem teljesül, sőt fordítva igaz.  Ezért megpróbálunk egy olyan
közbülső állapotot felírni, ami a $Q$-ból könnyedén (egy értékadással) elérhető és
ugyanakkor ez a kívánt feltétel teljesül rá.  Amennyiben ez sikerül, akkor már csak egy
szekvencia közbülső feltételeként kell pillantani erre az új $Q'$ feltételre
és máris felírható lesz a kívánt program egy értékadás és egy ciklus szekvenciájaként.

$Q' = (Q \es o=\hamis \es k=x.hib+1)$

Látható, hogy $Q' \kov P$ és $Q \kov \lf(o,k:=\hamis,x.hib+1, Q') = Q$.

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{o,k:=\hamis,x.hib+1}
  \begin{WHILE}{1}{\stm{\dots}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklketto \\
Ez a feltétel kezünkbe adja a ciklusfeltételt, hiszen $P$ és $R$ összehosonlításából
$\nem\pi$-re $k=x.lob$ adódik.  Tehát $\pi = (k\ne x.lob)$.
\begin{stuki}
  \stm{o,k:=\hamis,x.hib+1}
  \begin{WHILE}{1}{\stm{k\ne x.lob}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}

\cklharom \\
$t:=k-x.lob$ választással ez az állítás triviálisan teljesül.

\cklot \\
Előrevéve az utolsó feltételt már most biztosíthatjuk, hogy a programunk lefutása
véges legyen.  $S_0:=(k:=k-1)$\\
$P\es\pi\es k-x.lob=t_0 \kovkerdes\lf(S_0, k-x.lob<t_0)=
k-1-x.lob<t_0 \surd$

\cklnegy \\
Könnyedén látható, hogy a jelenlegi ciklusmag ezt a feltételt nem teljesíti, hiszen \\
$\lf(S_0, P)=\left( Q \es k-1\in[x.lob..x.hib+1] \es
  \sum\limits_{i\in[k-1..x.hib]} 10^{x.hib-i}(x[i]+y[i])=10^{x.hib-k+2}*\chi(o)+
  \sum\limits_{i\in[k-1..x.hib]}10^{x.hib-i}z[i] \right)$
$=: Q''$, nem következik $P \es \pi$-ből.

Ezért egy szekvencia második fele lesz az eddigi ciklusmag és $Q''$-t kell elérni az első
felében.  Ehhez vezessük be a $Q'''$ állítást a következőképpen:\\
$Q''':=(P\es\pi\es s=\chi(o)+x[k-1]+y[k-1])=\\ (Q \es k\in[x.lob+1..x.hib+1] \es
  \sum\limits_{i\in[k..x.hib]} 10^{x.hib-i}(x[i]+y[i])=10^{x.hib-k+1}*\chi(o) + 
  \sum\limits_{i\in[k..x.hib]}10^{x.hib-i}z[i] \\ \es s=\chi(o)+x[k-1]+y[k-1])$

A most bevezetett új állapot az alábbi elágazással elérhető $P\es\pi$-ből:
\begin{stuki}
  \begin{IF}{1}{\stm{o}}
    \stm{s:=1+x[k-1]+y[k-1]}
    \ELSE
    \stm{s:=x[k-1]+y[k-1]}
  \end{IF}
\end{stuki}

Hiszen:\\
\elagegy{P\es\pi} Nyilván teljesül.\\
\elagketto{P\es\pi}{Q'''}
\begin{enumerate}
\item{$o$:} $P\es\pi\es o \kovkerdes P\es\pi\es 1+x[k-1]+y[k-1]=\chi(o)+x[k-1]+y[k-1]\surd$
\item{$\nem o$:} $P\es\pi\es \nem o \kovkerdes P\es\pi\es x[k-1]+y[k-1]=\chi(o)+x[k-1]+y[k-1]\surd$
\end{enumerate}

Már csak a $Q'''$ és a $Q''$ állapotot kell programmal összekötnünk, szerencsére
ez egy értékadással megtehető:\\
$Q''' \kovkerdes \lf(o,z[k-1]:=s\ge10, s \textrm{ mod } 10, Q'')=
Q \es k-1\in[x.lob..x.hib+1] \es
  \sum\limits_{i\in[k-1..x.hib]} 10^{x.hib-i}(x[i]+y[i])=10^{x.hib-k+2}*\chi(s\ge 10)+
  \sum\limits_{i\in[k..x.hib]}10^{x.hib-i}z[i] + 10^{x.hib-k+1}(s\textrm{ mod }10)
$

Itt két lehetőséget kell megkülönböztetnünk:
\begin{enumerate}
\item{$\nem o$ (vagyis $\chi(o)=0)$:} $Q \es k\in[x.lob+1..x.hib+1] \es
  \sum\limits_{i\in[k..x.hib]} 10^{x.hib-i}(x[i]+y[i])= 
  \sum\limits_{i\in[k..x.hib]}10^{x.hib-i}z[i] \\ \es s=x[k-1]+y[k-1])
  \kovkerdes
  Q \es k-1\in[x.lob..x.hib+1] \es
  \sum\limits_{i\in[k-1..x.hib]} 10^{x.hib-i}(x[i]+y[i])=10^{x.hib-k+2}*\chi(s\ge 10)+
  \sum\limits_{i\in[k..x.hib]}10^{x.hib-i}z[i] + 10^{x.hib-k+1}(s\textrm{ mod }10)$, azaz
  igaz-e, hogy $10^{x.hib-k+1}(x[k-1]+y[k-1])=10^{x.hib-k+2}*\chi(x[k-1]+y[k-1]\ge 10)+
  10^{x.hib-k+1}(x[k-1]+y[k-1]\textrm{ mod }10)$, mivel $x[k-1]+y[k-1]\le 18$ az állítás igaz.
\item{$o$ (vagyis $\chi(o)=1$):} hasonlóan.
\end{enumerate}

\begin{stuki}
  \stm{o,k:=\hamis,x.hib+1}
  \begin{WHILE}{4}{\stm{k\ne x.lob}}
    \begin{IF}{1}{\stm{o}}
      \stm{s:=1+x[k-1]+y[k-1]}
      \ELSE
      \stm{s:=x[k-1]+y[k-1]}
    \end{IF}
    \stm{o,z[k-1]:=s\ge10, s \textrm{ mod } 10}
    \stm{k:=k-1}
  \end{WHILE}
\end{stuki}
\begin{textblock}{1}(2.4,-2.34)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{2.85cm}\\$R$
\end{textblock}
\begin{textblock}{1}(10.4,-1.64)
$P \es \pi$
\vspace{0.9cm}\\$Q'''$
\vspace{0.2cm}\\$Q''$
\end{textblock}

\end{document}