\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 18. feladat, adatabsztrakcióval}
\newcommand{\U}{\mathbb{U}}
\newcommand{\Y}{\mathbb{Y}}
\newcommand{\azon}{\text{azon}}
\newcommand{\ossz}{\text{ossz}}
\newcommand{\tipus}{\text{tipus}}
\renewcommand{\T}{\mathbb{T}}
\begin{document}
\noindent
\emph{Feladat:} Adott egy szekvenciális file (megengedett művelet az
$sx,dx,x:\Read$), ami egy bank tranzakcióit tartalmazza: egy ügyfél
adatait tartalmazó rekord után olyan rekordok következnek, amelyek az
ügyfél tranzakcióit írják le.
\begin{itemize}
\item Ügyfél=(Azonosító, Számla összege)
\item Tranzakció=(Kivét-betét, Összeg)
\end{itemize}
Állítsuk elő azt a file-t, ami az ügyfeleknek a bankban levő
pillanatnyi összegeit tartalmazza az ügyfél típusú rekordokban!

\emph{Specifikáció:}\\
$\U = (\azon:\N, \ossz: \Z)$\\
$\T = (\tipus:\{\text{kivét},\text{betét}\}, \ossz: \N)$\\
$\R = (u:\U;t:\T)$\\
$\F = \file(\R)$\\
$\F' = \file(\U)$\\
$A = \alatt{\F}{x} \times \alatt{\F'}{z}$\\
$B = \alatt{\F}{x'}$\\
$Q = ( x=x' \es ( x'.lov.u \vagy x'.dom=0))$\\

Az előfeltételben szereplő $x'.lov.u$. mivel $\R$ egy egyesítés, pont azt
fejezi ki, hogy a bemeneti file első rekordja ügyfél rekord kell, hogy legyen.

Most azonban át kell térnünk másik állapottérre, mivel a feladatot
sokkal könnyebben (egy identikus egyváltozós-egyértékű elemenkénti
feldolgozással) meg tudnánk oldani, ha a bemeneti file a jelenlegi
állapotot tartalmazná egyszerű ügyfél rekordok formájában.

\begin{textblock}{3}(5.0,-3.3)
$A' = \alatt{\F'}{t} \times \alatt{\F'}{z}$\\
$B' = \alatt{\F'}{t'}$\\
$Q' = ( t=t' )$\\
$R' = ( z=t' )$\\
\end{textblock}

\begin{textblock}{1}(8.0,-4.3)
\begin{stuki}[6cm]
  \stm{z:=<>}
  \stm{\open(t)}
  \stm{st,dt,t:\Read}
  \begin{WHILE}{2}{\stm{st=\norm}}
    \stm{z:\hiext(dt)}
    \stm{st,dt,t:\Read}
  \end{WHILE}
\end{stuki}
\end{textblock}

Lássuk mi a kapcsolat $\F$ és $\F'$ között!

Ehhez először egy $y\in\Y=\file((u:\U,t:\seq(\T)))$ file-á
transzformáljuk $\F$-et, ezen file lényege, hogy minden egyes
ügyfélhez egy rekordot tartalmaz, amely rekord első komponense az
ügyél azonosítója és nyitóösszege, második komoponense a tranzakciók
sorozata.  Azt, hogy az adatok a transzformáció közben nem romlanak
el, a $\seq(y|\{\U,\T\})=\seq(x|\{\U,\T\})$ kikötéssel írjuk le.

Ebből az $y$-ból már fel lehet írni, hogy miként érhető el $t$:\\
$dom(t)=dom(y)$\\
$\forall i\in[1,dom(t)]:t_i.\azon = y_i.u.\azon \es t_i.\ossz=y_i.u.\ossz+\sum\limits_{j=1}^{dom(y_i.t)}y_i.t_j.\ossz*\xi(y_i.t_j.\tipus)$, ahol \\
\[
\xi(t):= \left\{
\begin{array}{ll}
-1 & \text{, ha } t=\text{kivét} \\
1 & \text{, ha } t=\text{betét}
\end{array}
\right.
\]

A $t$ absztrakt file invariánsa legyen a következő: $sx=norm\nyil
dx.u$.  Ez kezdetben teljesül a $Q$ miatt, ha egy olvasást
végrehajtunk az $\open(t)$-ben.

\begin{textblock}{1}(7.0,-9.5)
\begin{stuki*}[4cm]{open($t$)}
  \stm{sx,dx,x:\Read}
\end{stuki*}
\end{textblock}


Az absztrakt read már bonyolultabb:

\begin{stuki*}[16cm]{$st,dt,t$:read}
  \begin{IF}[80]{7}{\stm{sx=\norm}}
    \stm{st:=\norm}
    \stm{dt:=dx_u}
    \stm{sx,dx,x:\Read}
    \begin{WHILE}{3}{\stm{sx=\norm \es dx.t}}
      \begin{IF}{1}{\stm{dx_t.\tipus=\text{betét}}}
        \stm{dt.\ossz:=dt.\ossz+dx_t.\ossz}
        \ELSE
        \stm{dt.\ossz:=dt.\ossz-dx_t.\ossz}
      \end{IF}
      \stm{sx,dx,x:\Read}
    \end{WHILE}
    \ELSE
    \stm{st:=\abnorm}
  \end{IF}
\end{stuki*}
\end{document}