\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 29. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adott az $x$ vektorban egy szöveg.  Állapítsuk meg,
hogy a szöveg tartalmaz-e magánhangzót!

\emph{Specifikáció:}\\
$V = \vect(\Z, Ch)$\\
$A = \alatt{\V}{x} \times  \alatt{\L}{l}$\\
$B = \alatt{\V}{x'}$\\
$Q = ( x=x' )$\\
$R = ( Q \es l=(\exists j\in[x.lob..x.hib]:(\text{magánhangzó}(x[j])) )$

Ha specifikációban szereplő magánhangzó logikai függvény nem
megengedett, akkor azt egyszerűen az $x[j]=``a'' \vagy x[j]=``e''
\vagy x[j]=``i'' \vagy x[j]=``o'' \vagy x[j]=``u''$ diszjunkcióval is
helyettesíthetjük angol szövegek esetén.  Magyar szövegek
feldolgozásakor ebbe a diszjunkcióba bele kell venni az ékezeteket is.

A lineáris keresés 2.8 specifikációja hasonló.  Lássuk,
hogy az alábbi átnevezés után milyen különbségek maradnak:

\begin{tabular}{ccc}
feladat &  & lin. ker. 2.8 \\
\hline
$x.lob$ & \knyil & $m$ \\
$x.hib$ & \knyil & $n$ \\
$\text{magánhangzó}(x[i])$ & \knyil & $\beta(i)$
\end{tabular}

A különbség, hogy $i$-t, azaz azt az eredménykomponenst, ami mutatná a
megtalált magánhangzó helyét az állapotterünk nem is tartalmazza.  Ez
a különbség persze indukálja, az utófeltétel összes olyan tagjának
kiesését is, ami $i$-re tett kikötést.  Tehát ez egy alteres
általánosított visszavezetés.

\begin{stuki}
  \stm{i,l:=x.lob-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es i \ne x.hib}}
    \stm{l:=\text{magánhangzó}(x[i+1])}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

\end{document}