\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 6. feladat}
\begin{document}
\noindent
\emph{Feladat:} Határozzuk meg az $n$ természetes szám osztóinak a számát!

\emph{Specifikáció:}\\
$A = \alatt{\N}{n} \times \alatt{\N_0}{d}$\\
$B = \alatt{\N}{n'}$\\
$Q = ( n=n' )$\\
$R = ( Q \es d=\sum\limits_{i=1}^n\chi(i\mid n))$

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

\begin{tabular}{ccc}
feladat &  & számlálás \\
\hline
$1$ & \knyil & $m$ \\
$i\mid n$ & \knyil & $\beta(i)$
\end{tabular}

Ez a visszavezetés majdnem természetes visszavezetés.  Bökkenő,
hogy a felhasználni kívánt programozási tétel specifikációjában
szereplő állapottér bővebb a feladatunk állapotterénél.  Tehát a
mi feladatunk állapottere altere a programozási tétel állapotterének.
Ezért hívjuk az ezzel a tulajdonsággal rendelkező visszavezetést
\emph{alteres} visszavezetésnek.  Az alteres visszavezetéseknek két
fajtája van, ez most a \emph{konstanssal helyettesítés}.  Erről
akkor beszélünk, ha a feladat állapotteréből olyan komponens
hiányzik, amit a programozási tétel programja nem változtatna meg.
Ekkor ugyanis az a változó nyilván helyettesíthető akár egy
konstanssal is a visszavezetés során.

Ellenőrízni szükséges, hogy a konstans érték, amivel $m$-et
helyettesítettük teljesíti-e a számlálás előfeltételének rá
vonatkozó nem triviális részét ($(m\le n+1)=(1\le n+1) (n\in\N) \surd$).

Ezekkel a megjegyzésekkel mostmár felírhatjuk a megoldó programot:

\begin{stuki}[6cm]
  \stm{k,d:=0,0}
  \begin{WHILE}{3}{\stm{k \ne n}}
    \begin{IF}{1}{\stm{k+1\mid n}}
      \stm{d:=d+1}
      \ELSE
      \SKIP
    \end{IF}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

\end{document}