\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 50. feladat}
\begin{document}
\noindent
\emph{Feladat:} Keressük meg az $[m..n]$ intervallumban azt a
legkisebb $k$ számot, amire $p$ és $k$ relatív prímek!

\emph{Specifikáció:}\\
$A = \alatt{\N}{m} \times \alatt{\N}{n} \times \alatt{\N}{k} \times \alatt{\L}{l} \times \alatt{\N}{p}$\\
$B = \alatt{\N}{m'} \times \alatt{\N}{n'} \times \alatt{\N}{p'}$\\
$Q = ( n=n' \es m=m' \es m\le n+1 \es p=p' )$\\
$R = ( Q \es l=(\exists j\in[m..n]:\lnko(p,j)=1) \es l\nyil(k\in[m..n] \es 
\lnko(p,k)=1 \es \forall j\in[m..k-1]:\lnko(p,j)\ne 1 ) )$

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
$k$ & \knyil & $i$ \\
$\lnko(p,i)=1$ & \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 $p$ az előfeltétel szerint adott értékű és a program során
nem változik (az utófeltételben is szerepel rejtve a $p=p'$).
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}
  \stm{k,l:=m-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es k \ne n}}
    \stm{l:=(\lnko(p,k+1)=1)}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

\end{document}