% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 7. feladat}
\def\nemosztja{\nmid}
\def\osztja{\mid}
\begin{document}
\noindent
\emph{Feladat:} Állapítsuk meg, hogy az $n$ természetes számnak van-e
páratlan valódi osztója!

\emph{Specifikáció:}\\
$A = \alatt{\N}{n} \times \alatt{\L}{l}$\\
$B = \alatt{\N}{n'}$\\
$Q = ( n=n' )$\\
$R = ( Q \es l=(\exists i\in[2,n-1]: i\osztja n \es 2\nemosztja i) )$

A specifikáció nagyon hasonló a lineáris keresés 2.8 tételéhez.  Az
eltéréseket az alábbi táblázattal foglalhatjuk össze:

\begin{tabular}{ccc}
feladat &  & lin. ker. 2.8 \\
\hline
$2$ & \knyil & $m$ \\
$n-1$ & \knyil & $n$ \\
$i\osztja n \es 2\nemosztja i$ & \knyil & $\beta(i)$
\end{tabular}

Alteres a visszavezetés, mert konstanssal helyettesítettük az $m$
állapottérkomponenst, illetve az $i$ eredménykomponensre vonatkozó
kikötéseink sem szerepelnek az utófeltételben, tehát az alteresség
általános esete is fennáll.

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

\end{document}