\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 21. feladat, adatabsztrakcióval}
\newcommand{\KN}{\text{KN}}
\newcommand{\VN}{\text{VN}}
\newcommand{\NEV}{\text{NEV}}
\newcommand{\U}{\mathbb{U}}
\newcommand{\Y}{\mathbb{Y}}
\newcommand{\Ch}{\text{Ch}}
\renewcommand{\T}{\mathbb{T}}
\begin{document}
\noindent
\emph{Feladat:} Adott az $x$ szekvenciális file (megengedett művelet
az $sx,dx,x:\Read$), melynek elemei egy vezetéknevet és egy
keresztnevet tartalmaznak.  A file a keresztnevek szerint rendezett.
Gyűjtsük ki a file-ból a különböző keresztneveket, és azt, hogy
hányszor szerepelnek.

\emph{Specifikáció:}\\

$\KN = (\seq(\Ch))$\\
$\VN = (\seq(\Ch))$\\
$\NEV = (vn:\VN, kn:\KN)$\\
$\F = \file(\NEV)$\\
$I_\F{f}=(\forall i\in[1,dom(f)-1]: f_i.kn\le f_{i+1}.kn)$\\
$\U = (kn:\KN, d:\N)$\\
$\F' = \file(\U)$\\
$A = \alatt{\F}{x} \times \alatt{\F'}{z}$\\
$B = \alatt{\F}{x'}$\\
$Q = ( x=x' )$\\

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 már az
eredménnyel egyenlő $\U$ tipusú rekordokat tartalmazná.

\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(\seq(\KN))$ file-á transzformáljuk
$\F$-et, ezen file lényege, hogy az azonos keresztnevek csoportosítva
vannak sorozatokba.  Azt, hogy a keresztnevek a transzformáció közben
nem romlanak el, a $\seq(y|\{\KN\})=\seq(x|\{\KN\})$ kikötéssel írjuk
le.  Kikötjük még, hogy ezen az állapotteren az input file-ban a
sorozatok nem üresek és első elemeik egymáshoz képest már szigorúan
növekvőek, azaz: $I_\Y(y)=(dom(y.hiv)>0 \es \forall i\in[1,dom(y)-1]:
dom(y_i)>0 \es {y_i}_1.kn<{y_{i+1}}_1.kn)$.

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.kn = {y_i}_1.kn \es t_i.d={y_i}.dom$

A $t$ absztrakt file invariánsa legyen a következő: $sx=norm\nyil
(dx.kn \ne dt.kn)$.\\ Ez kezdetben
teljesül ha olvasunk egyet, így az
$\open(t)$:
\begin{stuki*}{$\open(t)$}
\stm{sx,dx,x:\Read}
\stm{dt.kn,dt.d:=\text{``üres''},0}
\end{stuki*}

Az absztrakt read:

\begin{stuki*}[10cm]{$st,dt,t$:read}
  \begin{IF}[70]{6}{\stm{sx=\norm}}
    \stm{st:=\norm}
    \stm{dt.kn,dt.d:=dx.kn,1}
    \stm{sx,dx,x:\Read}
    \begin{WHILE}{2}{\stm{sx=\norm \es dt.kn\ne dx.kn}}
      \stm{dt.d:=dt.d+1}
      \stm{sx,dx,x:\Read}
    \end{WHILE}
    \ELSE
    \stm{st:=\abnorm}
  \end{IF}
\end{stuki*}
\end{document}