% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 31. feladat, adatabsztrakcióval}
\renewcommand{\P}{\mathbb{P}}
\renewcommand{\D}{\mathbb{D}}
\newcommand{\Hh}{\mathbb{H}}
\newcommand{\NEV}{\text{NÉV}}
\newcommand{\EHA}{\text{EHA}}
\newcommand{\nev}{\text{név}}
\newcommand{\eha}{\text{eha}}
\renewcommand{\T}{\mathbb{T}}
\newcommand{\E}{\mathbb{E}}
\begin{document}
\noindent

Adott az $x$ szekvenciális input fájl (megengedett művelet az $sx, dx,
x\colon read$), ami egy bevezetés a programozáshoz csoport elért
eredményeit tartalmazza.  Egy hallgató nevét és EHA kódját tartalmazó
rekord után mindig a ZH-inak és a plusz--mínusz dolgozatainak
eredményei következnek dolgozatonként külön-külön rekordban (ezek a
rekordok idő sorrendben vannak, tehát vegyesen a ZH-k és a
plusz-mínuszok, azonban természetesen mindegyik még a következő
hallgató neve előtt).  Tegyük fel, hogy mindenki \hbox{maximum} 3 dolgozatot
írt (senki nem írt pótdolgozatot), az elérhető 180 pontszám azok
egyszerű összege.  Azt is tegyük fel, hogy a gyakorlatvezető (gondolva
a későbbi feldolgozásra) az olyan plusz--mínusz dolgozatok eredményét
is rögzítette mínuszként, amikor a hallgató nem jelent meg.

\emph{Feladat:}
Adjuk meg azon hallgatók számát, akik nem teljesítik a plusz--mínusz
követelményt, de a ZH pontszámuk elégséges lenne a félév
teljesítéséhez (>=61)!

\emph{Specifikáció:}\\
$\Hh = (\nev\colon\NEV, \eha\colon \EHA)$\\
$I_\EHA(\eha) = (\tau(\eha)=7)$\\
$\P = \{-1, 0, 1\}$\\
$\D = [0, 60]$\\
$\R = (h:\Hh;p:\P;d:\D)$\\
$\F = \file(\R)$\\
$I_\F(f) = (\dom(f)>0 \nyil \lov(f).h)$\\
$A = \alatt{\F}{x} \times \alatt{\N_0}{d}$

Most át kell térnünk másik állapottérre, mivel a feladatot sokkal
könnyebben (egy számlálással) meg tudnánk oldani, ha a bemeneti file
($\F'=file(\E)$) a hallgatók összesített eredményeit tartalmazná, azaz
benne minden hallgatóhoz egy $\E = (h:\Hh, p:\Z, d:\N_0)$ rekord
tartozna.

\begin{textblock}{5}(3.4,-3.0)
$A' = \alatt{\F'}{t} \times \alatt{\N_0}{d}$\\
$B' = \alatt{\F'}{t'}$\\
$Q' = ( t=t' )$\\
$R' = ( d= \sum\limits_{i=1}^{dom(t')}\chi({t'}_i.p<0 \es {t'}_i.d>60) )$\\
\end{textblock}

\begin{textblock}{1}(8.0,-3.6)
\begin{stuki}[6cm]
  \stm{d:=0}
  \stm{\open(t)}
  \stm{st,dt,t:\Read}
  \begin{WHILE}{3}{\stm{st=\norm}}
    \begin{IF}{1}{\stm{dt.p<0 \es dt.d>60}}
      \stm{dt:=dt+1}
      \ELSE
      \SKIP
    \end{IF}
    \stm{st,dt,t:\Read}
  \end{WHILE}
\end{stuki}
\end{textblock}

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

Ehhez először egy $y\in\F''=\file((h:\Hh,s:\seq((p:\P;d:\D))))$ fájlá
transzformáljuk $\F$-et, ezen file lényege, hogy minden egyes
hallgatóhoz egy rekordot tartalmaz, amely rekord első komponense a
hallgató neve és EHA kódja, második komponense a dolgozat eredmények
sorozata (tehát a sorozat alaptípusa a plusz--mínusz és a ZH
eredmények egyesítése).  Azt, hogy az adatok a transzformáció közben
nem ``romlanak el'', a $\seq(y|\{\Hh,\P,\D\})=\seq(x|\{\Hh,\P,\D\})$ 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.h = y_i.h \es t_i.p=\sum\limits_{j=1}^{dom(y_i.s)}\xi(y_i.s_j) \es t_i.d=\sum\limits_{j=1}^{dom(y_i.s)}\varphi(y_i.s_j)$, ahol \\
$$
\xi(u) =
\begin{cases}
  0, &\text{ha } u.d, \\
  u_p, &\text{ha } u.p.
\end{cases}\text{, illetve }
\varphi(u) =
\begin{cases}
  0, &\text{ha } u.p, \\
  u_d, &\text{ha } u.d.
\end{cases}
$$

A $t$ absztrakt file invariánsa legyen a következő: $sx=norm\nyil
dx.h$.  Ez kezdetben teljesül az $I_\F$ miatt, ha egy olvasást
végrehajtunk az $\open(t)$-ben.  Az absztrakt readnek pedig a leírt
függvényeket kell kiszámolnia, a következő hallgató név, eha
rekordjáig vagy a fájl végéig.

\begin{center}
  \begin{tabular}{cc}
    \begin{minipage}{4cm}
      \begin{stuki*}[3cm]{open($t$)}
        \stm{sx,dx,x:\Read}
      \end{stuki*}
    \end{minipage}
    &
    \begin{minipage}{11cm}
      \begin{stuki*}[10cm]{$st,dt,t$:read}
        \begin{IF}[80]{7}{\stm{sx=\norm}}
          \stm{st:=\norm}
          \stm{dt.h,dt.p,dt.d:=sx.h,0,0}
          \stm{sx,dx,x:\Read}
          \begin{WHILE}{3}{\stm{sx=\norm \es \nem dx.h}}
            \begin{IF}{1}{\stm{dx.p}}
              \stm{dt.p:=dt.p+dx_p}
              \ELSE
              \stm{dt.d:=dt.d-dx_d}
            \end{IF}
            \stm{sx,dx,x:\Read}
          \end{WHILE}
          \ELSE
          \stm{st:=\abnorm}
        \end{IF}
      \end{stuki*}
    \end{minipage}
  \end{tabular}
\end{center}
\end{document}