% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 2008.,  6. ZH feladatai, adatabsztrakció}
\begin{document}
\noindent
Egy file-nak azt a szakaszát, amely csupa negatív elemet tartalmaz
úgy, hogy a szakaszt jobbról és balról nemnegatív elem, vagy a file
vége határolja, a file negatív szigetének nevezzük.

\emph{1. feladat:} Számoljuk meg egy $sx,dx,x:\Read$ művelettel
ellátott file-ban a negatív szigetek számát!

\emph{2. feladat:} Állítsuk elő azt az $y$ kimeneti file-t, ami az $sx,dx,x:\Read$
művelettel ellátott file-hoz a benne lévő szigetek hosszát tartalmazza.
Péládul az $x=<0, -1, -4, 6, 1, -3>$ file-hoz az $y=<2, 1>$ file-t kell előállítani!

\emph{Megoldás:}\\
$x\in\file(\Z)$

Adjunk az $x$ file-hoz egy olyan absztrakciót, ami csak a negatív
szigetek hosszát tartalmazza, mint ahogy a második feladathoz adott
példában van!

Ehhez először csoportosítsuk sorozatokba az egymás mellett lévő
negatív és nemnegatív elemeket, majd ezekből csak a negatívokat
hagyjuk meg és vegyük ezen sorozatok hosszát.

\newcommand{\POZ}{\text{POZ}}
\newcommand{\NEG}{\text{NEG}}
$\POZ = \seq(\Z \setminus \{i\in\Z \mathop{|} i<0\})$, 
$\NEG = \seq(\Z \setminus \{i\in\Z \mathop{|} i\ge0\})$\\
$w\in\file((p:\POZ;n:\NEG)), I(w) = (\forall i\in[1, \dom(w)-1]: w_i.p\ne w_{i+1}.p)$\\
$\seq(w|\{\POZ, \NEG\}) = x$

Az invariánssal azt zártuk ki, hogy két csak negatívokból álló sorozat
álljon egymás után közvetlenül.  A szekvenciális megfelelővel pedig
könnyedén fel tudtuk írni a két állapottér közti összefüggést,
nevezetesen azt, hogy a számok tekintetében a fájlok megegyeznek.

A következő absztrakcióban már csak a negatív sorozatok szerepeljenek:
$z\in\file(\NEG), z=\seq(w| \NEG)$

\renewcommand{\T}{\mathbb{T}}
Végül ezen sorozatoknak csak a hossza alkossa azt az absztrakciós
szintet, amin majd a feladatainkat már megoldjuk: $t\in\file(\N)=\T,
\dom(t)=\dom(z), \forall i\in [1,\dom(t)]: t_i= |z_i|$

Az első feladat megoldása az összegzés tételére vezethető vissza a
konstans $f\equiv 1$ függvénnyel, a második pedig az elemenkénti
feldolgozásra, identikus leképezéssel.

\begin{tabular}{ccc}
\parbox{5cm}{
$A = \alatt{\T}{t} \times \alatt{\N_0}{d}$\\
$B = \alatt{\T}{t'}$\\
$Q = ( t=t' )$\\
$R = ( d=\sum\limits_{i=1}^{\dom(t')}1)$

\begin{stuki}[4cm]
  \stm{\open(t)}
  \stm{st,dt,t:\Read}
  \stm{d:=0}
  \begin{WHILE}{2}{\stm{st}}
    \stm{d:=d+1}
    \stm{st,dt,t:read}
  \end{WHILE}
\end{stuki}
} & \parbox{5cm}{
$A = \alatt{\T}{t} \times \alatt{\T}{y}$\\
$B = \alatt{\T}{t'}$\\
$Q = ( t=t' )$\\
$R = ( y=t')$

\begin{stuki}[4cm]
  \stm{\open(t)}
  \stm{st,dt,t:\Read}
  \stm{y:=<>}
  \begin{WHILE}{2}{\stm{st}}
    \stm{y:\hiext(dt)}
    \stm{st,dt,t:\Read}
  \end{WHILE}
\end{stuki}
} & \parbox{5cm}{\begin{stuki*}[5cm]{open($t$)}
  \stm{sx,dx,x:\Read}
  \begin{WHILE}{1}{\stm{sx \es dx\ge0}}
    \stm{sx,dx,x:\Read}
  \end{WHILE}
\end{stuki*}
\begin{stuki*}[6cm]{$st,dt,t:$read}
    \begin{IF}{8}{\stm{sx}}
      \stm{st:=\norm}
      \stm{dt:=1}
      \stm{sx,dx,x:\Read}
      \begin{WHILE}{2}{\stm{sx \es dx<0}}
        \stm{dt:=dt+1}
        \stm{sx,dx,x:\Read}
      \end{WHILE}
      \begin{WHILE}{1}{\stm{sx \es dx\ge0}}
        \stm{sx,dx,x:\Read}
      \end{WHILE}
      \ELSE
      \stm{st:=\abnorm}
    \end{IF}
\end{stuki*}
}
\end{tabular}

\end{document}