\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 27. feladat}
\begin{document}
\noindent
\emph{Feladat:} Keressük meg az $[a,b]$ intervallumon
értelmezett, egész értékű $f$ függvénynek az első $n$-nél kisebb vagy
0 értékét!

\emph{Specifikáció:}\\
$A = \alatt{\Z}{a} \times \alatt{\Z}{b} \times \alatt{\Z}{n} \times \alatt{\Z}{i} \times \alatt{\L}{l}$\\
$B = \alatt{\Z}{a'} \times \alatt{\Z}{b'} \times \alatt{\Z}{n'}$\\
$Q = ( a=a' \es b=b' \es a\le b+1 \es n=n')$\\
$R' = ( Q \es l=(\exists j\in[a..b]:(f(j)<n \vagy f(j)=0)) \es l\nyil(i\in[a..b] \es 
(f(i)<n \vagy f(i)=0) \es \forall j\in[a..i-1]:(f(j)\ne n \es f(j) \ne 0)))$

A specifikáció nagyon hasonló a lin. ker. 2.8 programozási tételéhez.  Az
eltéréseket az alábbi táblázattal foglalhatjuk össze:

\begin{tabular}{ccc}
feladat &  & lin. ker. 2.8 \\
\hline
$a$ & \knyil & $m$ \\
$b$ & \knyil & $n$ \\
$f(i)=0 \vagy f(i)<n$ & \knyil & $\beta(i)$
\end{tabular}

Ez a visszavezetés nem természetes, mert az állapottér bővebb és a
helyettesítő táblázatban a $\beta(i)$ helyettesítésekor fel is
használjuk ezt a plusz komponenst.  Ugyanakkor megjegyezhetjük, hogy a
bevezetett $n$ az előfeltétel szerint adott értékű és a program során
nem változik (az utófeltételben is szerepel rejtve a $n=n'$).
Amennyiben ezek a feltételek teljesülnek egy ilyen kiegészítő
komponensre, akkor őt a visszavezetés \emph{paraméterének} nevezzük,
mivel ilyenkor a visszavezetés \emph{paraméteres visszavezetés}.

\begin{stuki}[6cm]
  \stm{i,l:=a-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es i \ne b}}
    \stm{l:=(f(i+1)=0 \vagy f(i+1)<n)}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

A feladat azonban az volt, hogy az első $n$-nél kisebb vagy $0$
\emph{értéket} keressük meg, nem az argumentumot.  Azonban az
argumentumból az érték könnyen meghatározható (egy új $e$
állapottérkomponensbe):

$R=(R' \es l\nyil e=f(i))$

\begin{stuki}[6cm]
  \stm{i,l:=a-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es i \ne b}}
    \stm{l:=(f(i+1)=0 \vagy f(i+1)<n)}
    \stm{i:=i+1}
  \end{WHILE}
  \stm{e:=f(i)}
\end{stuki}


\end{document}