\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 14. feladat}
\begin{document}
\noindent
\emph{Feladat:} Állapítsuk meg, hogy van-e az $f$ függvény értékei
között páros szám!

\emph{Specifikáció:}\\
$A = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\L}{l}$\\
$B = \alatt{\Z}{m'} \times \alatt{\Z}{n'}$\\
$Q = ( n=n' \es m=m' \es m\le n+1)$\\
$R = ( Q \es l=(\exists j\in[m..n]:2|j) )$

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
$2|f(i)$ & \knyil & $\beta(i)$
\end{tabular}

A különbség, hogy az $i$-t, azaz azt az eredménykomponenst, ami
mutatná a megtalált páros elem 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 \emph{alteres visszavezetés}, hiszen a feladatunk
állapottere altere a programozási tétel állapotterének.  Ugyanakkor
itt most nem arról van szó, hogy azt a komponenest konstanssal
helyettesítettük volna.  Amikor a programozási tétel állapottérének
egy eredménykomponensét (tehát aminek kezdőértéke tetszőleges, de az
utófeltétel tesz rá kikötést) nem találjuk meg a feladat
állapotterében (és így természetesen az utófeltételében sem), akkor az
alteres visszavezetés \emph{általánosított} esetéről beszélünk.  (Más
terminológiák az ilyen visszavezetést egyszerűen az általánosított
visszavezetések közé is szokták sorolni, mondván, hogy az utófeltétel
gyengébb a tétel utófeltételénél.)

Természetesen a feladatot ekkor is úgy oldjuk meg, hogy a programozási
tételben írjuk át a táblázatunkban összeszedett változtatásokat és
végeredményben a megoldóprogram nem fog kisebb állapottéren futni.
Azt, hogy a program más eredményeket is elér, amire mi nem vagyunk
kíváncsiak, megtűrjük.

\begin{stuki}
  \stm{i,l:=m-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es i \ne n}}
    \stm{l:=2|f(i+1))}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

\end{document}