\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 18-19. feladat}
\newcommand{\db}{\text{db}}
\newcommand{\szj}{\text{szj}}
\renewcommand{\div}{\mathop{\text{ div }}}
\begin{document}
\noindent
\emph{Feladat:} Az $x$ egész számokból álló vektor egy decimális szám
számjegyeit tartalmazza helyiérték szerint csökkenõ sorrendben.
Állítsuk elõ $x$-ben az eredetinél eggyel nagyobb szám ugyanilyen
ábrázolását és mondjuk meg, volt-e túlcsordulás!

\emph{Feladat:} Az $x$ egész számokból álló vektor egy decimális szám
számjegyeit tartalmazza helyiérték szerint csökkenõ sorrendben.
Állítsuk elõ $x$-ben az eredetinél eggyel kisebb szám ugyanilyen
ábrázolását és mondjuk meg, volt-e alulcsordulás!

\emph{Specifikáció:}\\
$\V = \vect(\Z, [0..9])$\\
$A = \alatt{\V}{x} \times \alatt{\{-1,1\}}{y} \times \alatt{\L}{l}$\\
$B = \alatt{\V}{x'} \times \alatt{\{-1,1\}}{y'}$\\
$Q = ( x=x' \es y=y' )$\\
$R = ( y=y' \es f(x')+y = f(x) + y\cdot\chi(l)\cdot 10^{x.\dom})$, ahol \\
$f:\V\nyil\N_0$, $f(x)=\sum\limits_{k=0}^{x.\dom-1}(x_{x.\hib-k})\cdot 10^k$

Az $f$ függvény arra való, hogy egy vektor számérték megadja.
Amennyiben volt túlcsordulás, azt az $l$ jelzi és így az utófelététel
pont azt mondja, hogy amennyiben nem volt túlcsordulás, akkor az új
$x$ értéke az eredetinél eggyel nagyobb vagy kisebb ($y$
függvényében).  Ha volt túlcsordulás és $l$ igaz, akkor a $\chi(l)$
értéke 1, így az utófeltétel utolsó szorzata nem 0, hanem pont
korrigálja a túlcsordulást.

Tehát a két feladatot egyszerre úgy oldjuk meg, hogy az állapottér $y$
komponense jelzi, hogy növelésrõl vagy csökkentésrõl van szó.

\emph{Megoldás:}\\
$P = ( y=y' \es i\in[0,x.\dom] \es f(x')+y = f(x) + y\cdot\chi(l)\cdot 10^{i})$

Elsõ ránézésre talán nem érthetõ, hogy ez az utófeltétel miért
gyengíthetõ ilyen szépen invariánssá.  Azonban gondoljuk meg, hogy ha
az $x.\dom$ helyett egy kisebb (de 0-nál nagyobb) számot írunk, akkor
azzal úgy tekintünk a számra a korrigáló tényezõben, mintha az eleje
nem lenne a vektornak.  Az $f$ függvény pedig ugyanannyival növeli meg
mind a két oldalt, amikor a vektor elejét tekinti, hiszen ahhoz még
nem nyúltunk.  Ha pedig az $x.\dom$ helyett 0-át írunk, az egy nagyon
kényelmes kiinduló állapot, hiszen ekkor az $l$-et igazra választva az
egyenlõség két oldala pontosan megegyezik.

\cklegy\\
$Q' = (Q \es l=\igaz \es i=0)$

\cklketto\\
$\nem\pi = (x.\dom=i \vagy \nem l)$, a $\nem l$ valóban diszjunkcióba
vehetõ a triviálisan adódó $x.\dom=0$-val, ugyanis ha $l$ hamis, akkor
$\chi(l)$ 0, így $P$ és $R$ végébõl is kiesik az összeg második
tényezõje, a következés teljesülni fog.

\cklharom $\quad t:=x.\dom-i$

\cklnegyot\\
Négy (az állapotteret együttesen teljesen lefedõ) eset lehetséges:
\begin{enumerate}
\item $\underline{y=1 \es x_{x.\hib-i}=9}$, ekkor legyen az értékadás a következõ: $x_{x.\hib-i},i:=0, i+1$.  Ez helyes, ui.

$(P\es\pi\es t=t_0\es y=1 \es x_{x.\hib-i} = 9) = $ \\
$( y=y' \es i\in[0,x.\dom-1] \es f(x')+1 = \overset{
\sum\limits_{k=0}^{i-1}(x_{x.\hib-k})\cdot 10^k + 10^i + 9\cdot 10^i + \sum\limits_{k=i+1}^{x.\dom-1}(x_{x.\hib-k})\cdot 10^k
}{\overbrace{\sum\limits_{k=0}^{x.\dom-1}(x_{x.\hib-k})\cdot 10^k + 10^i}} \es x.\dom-i = t_0)$\\
$\Downarrow\surd$\\
$\lf(x_{x.\hib-i},i:=0, i+1, P\es t<t_0) = $ \\
$( y=y' \es i+1\in[0,x.\dom] \es f(x')+1 = \sum\limits_{k=0}^{i-1}(x_{x.\hib-k})\cdot 10^k + 10^{i+1} + \sum\limits_{k=i+1}^{x.\dom-1}(x_{x.\hib-k})\cdot 10^k \es x.\dom-i-1 < t_0)$

\item Hasonlóan levezethetõ, hogy $\underline{y=1 \es x_{x.\hib-i}\ne 9}$ esetben az $x_{x.\hib-i},i,l:=x_{x.\hib-i}+1, i+1, \hamis$ helyes,
\item $\underline{y=-1 \es x_{x.\hib-i} = 0}$ esetén az $x_{x.\hib-i},i:=9, i+1$,
\item míg $\underline{y=-1 \es x_{x.\hib-i}\ne 0}$ esetén az $x_{x.\hib-i}, i, l:= x_{x.\hib-i}-1, i+1, \hamis$.
\end{enumerate}

\begin{stuki}[16cm]
  \stm{i,l:=0, \igaz}
  \begin{WHILE}{3}{\stm{x.\dom \ne i \es l}}
    \begin{CASE}{2}{4}
       \WHEN{\stm{y=1 \es x_{x.\hib-i} = 9}}
       \stm{x_{x.\hib-i},i:=\\0, i+1}
       \WHEN{\stm{y=1 \es x_{x.\hib-i}\ne 9}}
       \stm{x_{x.\hib-i},i,l:=\\x_{x.\hib-i}+1, i+1, \hamis}
       \WHEN{\stm{y=-1 \es x_{x.\hib-i} = 0}}
       \stm{x_{x.\hib-i},i:=\\9, i+1}
       \WHEN{\stm{y=-1 \es x_{x.\hib-i}\ne 0}}
       \stm{x_{x.\hib-i},i,l:=\\x_{x.\hib-i}-1, i+1, \hamis}
     \end{CASE}
  \end{WHILE}
\end{stuki}
\end{document}
