\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 21. feladat max. ker., 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.
Adjuk meg, hogy melyik keresztnév fordul elõ a legtöbbször!

\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{\U}{max}$\\
$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 maximumkereséssel) meg tudnánk oldani, ha a
bemeneti file $\F'$ tipusú lenne, hiszen ekkor a rekordok második
részében szereplõ értékek között kereshetnénk a maximumot.

\begin{textblock}{2.5}(5.0,-3.3)
$A' = \alatt{\F'}{t} \times \alatt{\U}{max}$\\
$B' = \alatt{\F'}{t'}$\\
$Q' = ( t=t' \es t.dom>0)$\\
$R' = ( \exists i\in [1,dom(t)]: t_i=max \es \forall i\in [1,dom(t)]:t_i.d\le max.d )$\\
\end{textblock}

\begin{textblock}{1}(8.0,-4.3)
\begin{stuki}[6cm]
  \stm{\open(t)}
  \stm{st,dt,t:\Read}
  \stm{max:=dt}
  \begin{WHILE}{3}{\stm{st=\norm}}
    \begin{IF}{1}{\stm{dt.d\le max.d}}
      \SKIP
      \ELSE
      \stm{max:=dt}
    \end{IF}
    \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}
