\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 18. feladat, függvényabsztrakcióval}
\newcommand{\U}{\mathbb{U}}
\newcommand{\Y}{\mathbb{Y}}
\newcommand{\azon}{\text{azon}}
\newcommand{\ossz}{\text{ossz}}
\newcommand{\tipus}{\text{tipus}}
\newcommand{\RE}{\text{RE}}
\newcommand{\extr}{\text{extr}}
\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}$

\vspace{1cm}

A feladat állapotterét először áttranszformáljuk egy olyanra, ahol a
file végén van extremális elem, még mielőtt az olvasás során abnorm
értéket kapnánk, mert így könnyebb lesz felírni a kiértékelendő
rekurzív függvényt.

$\RE=\R \cup \{\extr\}, \F''=file(\RE)$\\
$A' = \alatt{\F''}{y} \times \alatt{\F'}{z}$\\
$y=\con(x,<\extr>)$

$B = \alatt{\F''}{y'}$\\
$Q = ( y=y' \es ( y.\lov.u \es y.\dom\ne 0))$\\
$R = ( z = f(\dom(y'))_1)$, ahol $f:[1,\dom(y')]\nyil \F'\times\N\times\Z, f(1):=(<>,y_1,0), \forall i\in[2,\dom(y')]: f(i):=F(i, f(i-1))$
\[
F(i,z):= \left\{
\begin{array}{ll}
(hiext(z_1,(z_2,z_3)), y_i.\azon, y_i.\ossz) & \text{, ha } y_i.u \\
(z_1, z_2, z_3 + y_i.\ossz) & \text{, ha } y_i.t \es y_i.\tipus = \text{betét} \\
(z_1, z_2, z_3 - y_i.\ossz) & \text{, ha } y_i.t \es y_i.\tipus = \text{kivét}
\end{array}
\right.
\]

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

\begin{textblock}{1}(7.0,-8.5)
\begin{stuki*}[4cm]{open($y$)}
  \stm{sx,dx,x:\Read}
  \stm{dy:=\_}
\end{stuki*}
\end{textblock}

\begin{textblock}{1}(6.0,-7.0)
\begin{stuki*}[9cm]{$sy,dy,y:\Read$}
\begin{IF}{4}{\stm{dy\ne\extr}}
  \stm{sy:=\norm}
  \begin{IF}{2}{\stm{sx=\norm}}
    \stm{dy:=dx}
    \stm{sx,dx,x:\Read}
    \ELSE
    \stm{dy:=\extr}
  \end{IF}
  \ELSE
  \stm{sy:=\abnorm}
\end{IF}
\end{stuki*}
\end{textblock}

A megoldóprogramot a rekurzív függvényérték kiszámításának tételével
kapjuk (az open utáni olvasás és kezdőértékadást az indokolja, hogy a
rekurziót csupán $f(2)$-től szeretnénk indítani, az $f(1)$ értékét
explicit definiáltuk):

\begin{stuki}[16cm]
  \stm{\open(y)}
  \stm{sy,dy,y:\Read}
  \stm{z,a,s:=<>,dy.\azon, dy.\ossz}
  \stm{sy,dy,y:\Read}
  \begin{WHILE}{3}{\stm{sy=\norm}}
    \begin{CASE}{1}{3}
      \WHEN{\stm{dy.u}}
      \stm{a,s:=dy.\azon,dy.\ossz}
      \WHEN{\stm{dy.t \es dy.\tipus = \text{betét}}}
      \stm{s:=s+dy.\ossz}
      \WHEN{\stm{dy.t \es dy.\tipus = \text{kivét}}}
      \stm{s:=s-dy.\ossz}
    \end{CASE}
    \stm{sy,dy,y:\Read}
  \end{WHILE}
\end{stuki}

Vegyük észre, hogy a kész programban sehol nem használtuk ki, hogy az
utolsó elem a speciális extr, így igazából az új típusra nincs is
szükség, azt is írhatjuk helyette, hogy 13, 0, mint ügyfél típusú
rekord.

\end{document}