% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 22. feladat, adatabsztrakcióval}
\newcommand{\SZO}{\text{SZO}}
\newcommand{\ELV}{\text{ELV}}
\newcommand{\U}{\mathbb{U}}
\begin{document}
\noindent
\emph{Feladat:} Adott egy karakterekből álló szekvenciális file
(megengedett művelet az $sx,dx,x:read$).  Számoljuk meg, hogy a
szövegben hány $k$ betűnél hosszabb szó van!  (A szavakat tetszőleges
számú szóköz választhatja el.)

\emph{Specifikáció:}\\
$\F = \file(Ch)$\\
$A = \alatt{\F}{x} \times \alatt{\N_0}{k} \times \alatt{\N_0}{d}$\\
$B = \alatt{\F}{x'} \times \alatt{\N_0}{k'}$\\
$Q = ( x=x' )$

A feladatot adatabsztrakcióval oldjuk meg, az absztrakt file
természetes számokból áll, amik a konkrét file szóhosszainak felelnek
meg.  A formális felírásban először egy olyan állapottérre térünk át,
ahol a file-ban a szavak és az elválasztó részek betűi sorozatokba
vannak csoportosítva, itt természetesen adódó invariáns, hogy csak az
szó- és szóközcsoportok egyesítéséből képzett file-ban egymást nem
követi két azonos típusú elem (hiszen azokat egy elemben is
tárolhatjuk).  Ezekután az elválasztórészeket elhagyjuk, majd az
utolsó transzformációs lépéssel alakítjuk a megmaradt szósorozatokat a
szóhosszaikat tartalmazó file-lá.

$Ch'=Ch\setminus\{\_\}, \SZO=\seq^+(Ch'), \ELV=\seq^+(\{\_\}), \S=(s:\SZO; e:\ELV), \U=\file(\S), \V=\seq(\SZO), \F' = \file(\N) $\\
$I_U(u)=\forall i\in [1,\dom(u)-1]: u_i.s\ne u_{i+1}.s$\\
$A'' = \alatt{\U}{u} \times \alatt{\N_0}{k} \times \alatt{\N_0}{d}$\\
$\seq(u|Ch)=\seq(x|Ch)$\\
$A''' = \alatt{\V}{v} \times \alatt{\N_0}{k} \times \alatt{\N_0}{d}$\\
$\seq(u|\SZO)=\seq(v|\SZO)$\\
$A' =\alatt{\F'}{t} \times \alatt{\N_0}{k} \times \alatt{\N_0}{d}$\\
$\dom(v)=\dom(t) \es \forall i\in[1,\dom(t)]:t_i=v_i.dom$

Az absztrakt read invariánsa: ha még van szó a konkrét fileban,
akkor annak első karakterén állunk.  Ennek megfelelően az absztrakt
open és read az alábbi:

\begin{textblock}{1}(6.0,-2.8)
\begin{stuki*}[6cm]{open(t)}
  \stm{sx,dx,x:read}
  \begin{WHILE}{1}{\stm{sx=norm \es dx=\_}}
    \stm{sx,dx,x:read}
  \end{WHILE}
\end{stuki*}
\end{textblock}

\begin{textblock}{1}(6.0,0.0)
\begin{stuki*}[8cm]{st,dt,t:read}
  \begin{IF}[70]{8}{\stm{sx=norm}}
    \stm{st:=norm}
    \stm{dt:=1}
    \stm{sx,dx,x:read}
    \begin{WHILE}{2}{\stm{sx=norm \es dx\ne\_}}
      \stm{dt:=dt+1}
      \stm{sx,dx,x:read}
    \end{WHILE}
    \begin{WHILE}{1}{\stm{sx=norm \es dx=\_}}
      \stm{sx,dx,x:read}
    \end{WHILE}
    \ELSE
    \stm{st:=abnorm}
  \end{IF}
\end{stuki*}
\end{textblock}

\vspace{8cm}

Ezzel az absztrakt file-lal a feladat már egyszerűen visszavezethető
egy összegzésre (ahol aszerint a függvény szerint összegzünk, ami csak
k-nál nagyobb argumentumra 1, egyébként 0).

$B = \alatt{\F'}{t'} \times \alatt{\N_0}{k'}$\\
$Q = ( t=t' )$\\
$R = ( d=\sum\limits_{i=t'.lob}^{t'.hib} f(t'_i) )$
\[
f(e)=
\left\{
\begin{array}{ll}
  1 & \text{, ha } e >k \\
  0 & \text{, egyébként}
\end{array}
\right.
\]

\begin{textblock}{1}(1.0,-6.0)
  \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>k}}
	\stm{d:=d+1}
	\ELSE
	\stm{d:=d+0}
      \end{IF}
      \stm{st,dt,t:read}
    \end{WHILE}
  \end{stuki}
\end{textblock}

\end{document}