\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