% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 6. feladat}
\def\nemosztja{\hskip-0.3em\not|\hskip0.2em}
\def\osztja{\hskip0.1em|\hskip0.1em}
\begin{document}
\noindent
\emph{Feladat:} Döntsük el, hogy a $x$ természetes szám prím szám-e!

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

\emph{Megoldás:}\\
A megoldás  egy ciklus lesz, a következő invariánssal:

$P = ( Q \es k\in[1,x-1] \es l=(\forall i\in[2,k]: i\nemosztja x) )$

Ellenőrízzük le a ciklus feltételeit:\\
\cklegy\\
Nem teljesül, ezért bevezetünk a szokásos módon egy
$$Q' = (Q \es k=1 \es l=\igaz) \kov P$$
állapotot, amire
$$Q \kov \lf(k,l:=1, \igaz, Q')$$
igaz.

\cklketto

$P$ és $R$ összehosonlításából $\nem\pi$-re $k=x-1 \vagy l=\hamis$
adódik.  Tehát $\pi = (k\ne x-1 \es l=\igaz)$.

\cklharom \\
Jelen esetben ez: $Q \es k\in [1,x-2] \es \ldots \kov t>0$. Tehát $t:=x-k$
egy megfelelő terminálófüggvény.

\cklnegyot \\
\begin{stuki*}[6cm]{$S_0$}
  \stm{l,k:=(k+1)\nemosztja x, k+1}
\end{stuki*}

$S_0$ valóban jó ciklusmag:

$Q \es k\in [1,x-2] \es l=\igaz \es l=(\forall i\in[2,k]: i\nemosztja
x) \kov Q \es k+1\in [1,x-1] \es (k+1)\nemosztja x=(\forall
i\in[2,k+1]: i\nemosztja x)$

Ezzel a ciklust levezettük.
\begin{stuki}[6cm]
  \stm{k,l:=1,\igaz}
  \begin{WHILE}{1}{\stm{k\ne x-1 \es l=\igaz}}
    \stm{l,k:=(k+1)\nemosztja x, k+1}
  \end{WHILE}
\end{stuki}

\end{document}