\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 20. feladat, adatabsztrakcióval}
\newcommand{\SZO}{\text{SZO}}
\newcommand{\ELV}{\text{ELV}}
\newcommand{\U}{\mathbb{U}}
\begin{document}
\noindent
\emph{Feladat:} Adott az $x$ szekvenciális file (megengedett művelet
az $sx,dx,x:read$), amely egy szöveget tartalmaz.  Állapítsuk meg,
hogy hány olyan szó van a szövegben, ami tartalmaz ``R'' betűt!

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

A feladatot adatabsztrakcióval oldjuk meg, az absztrakt file logikai
értékekből áll, amik a konkrét file szavainak felelnek meg.
Pontosabban az $i.$ logikai érték akkor és csak akkor igaz, ha a
konkrét fileban az $i.$ szóban van ``R'' betű.  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 logikai értékeket tartalmazó
file-lá.

$Ch'=Ch\setminus\{\_\}, \SZO=\seq^+(Ch'), \ELV=\seq^+(\{\_\}), \S=(s:\SZO; e:\ELV), \U=\file(\S), \V=\seq(\SZO), \F' = \file(\L) $\\
$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}{d}$\\
$\seq(u|Ch)=\seq(x|Ch)$\\
$A''' = \alatt{\V}{v} \times \alatt{\N_0}{d}$\\
$\seq(u|\SZO)=\seq(v|\SZO)$\\
$A' =\alatt{\F'}{t} \times \alatt{\N_0}{d}$\\
$\dom(v)=\dom(t) \es \forall i\in[1,\dom(t)]:t_i=(\exists j\in[1,v_i.dom]:{v_i}_j='R')$

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.9)
\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}(7.0,0.0)
\begin{stuki*}[8cm]{$st,dt,t$:read}
  \begin{IF}[70]{8}{\stm{sx=\norm}}
    \stm{st:=\norm}
    \stm{dt:=(dx=\text{``R''})}
    \stm{sx,dx,x:\Read}
    \begin{WHILE}{2}{\stm{sx=\norm \es dx\ne\_}}
      \stm{dt:=dt \vagy dx=\text{``R''}}
      \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 számlálásra:

$B = \alatt{\F'}{t'}$\\
$Q = ( t=t' )$\\
$R = ( d=\sum\limits_{i=t'.lob}^{t'.hib} \chi(t'_i) )$

\begin{textblock}{1}(0.0,-5.0)
\begin{stuki}[7cm]
  \stm{d:=0}
  \stm{\open(t)}
  \stm{st,dt,t:\Read}
  \begin{WHILE}{3}{\stm{st=\norm}}
    \begin{IF}{1}{\stm{dt}}
      \stm{d:=d+1}
      \ELSE
      \SKIP
    \end{IF}
    \stm{st,dt,t:\Read}
  \end{WHILE}
\end{stuki}
\end{textblock}


\end{document}