\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 2. feladat}
\begin{document}
\noindent
\emph{Feladat:} Határozzuk meg az $x$ és az $y$ természetes számok legnagyobb
közös osztóját!

\emph{Specifikáció:}\\
$A = \alatt{\N}{x} \times \alatt{\N}{y} \times \alatt{\N}{a} \times \alatt{\N}{b}$\\
$B = \alatt{\N}{x'} \times \alatt{\N}{y'}$\\
$Q = ( x=x' \es y=y' )$\\
$R = ( Q \es a=b=\lnko(x,y))$

A specifikációból kiolvasható, hogy az eredményt az állapottér két változója ($a$ és $b$)
is szolgáltatja.

\emph{Megoldás:}\\
Most keressük meg a specifikációnak megfelelő megoldó programot! A megoldást
úgy sejtjük, hogy egy ciklussal találhatjuk meg.  Nos, mi legyen ennek a
ciklusnak az invariánsa?

$P  = (Q \es a\in [1..x] \es b\in [1..y] \es \lnko(a,b)=\lnko(x,y))$

Ellenőrízzük le a ciklus feltételeit:\\
\cklegy \\
Jól láthatóan nem teljesül, sőt fordítva igaz.  Ezért megpróbálunk egy olyan
közbülső állapotot felírni, ami a $Q$-ból könnyedén (egy értékadással) elérhető és
ugyanakkor ez a kívánt feltétel teljesül rá.  Amennyiben ez sikerül, akkor már csak egy
szekvencia közbülső feltételeként kell pillantani erre az új $Q'$ feltételre
és máris felírható lesz a kívánt program egy értékadás és egy ciklus szekvenciájaként.

$Q' = (Q \es a=x \es b=y)$

Látható, hogy $Q' \kov P$ és $Q \kov \lf(a,b:=x,y , Q') = (Q \es x=x \es y=y) = Q \surd$.

Tehát a program valahogy így néz ki:
\begin{stuki}[6cm]
  \stm{a,b:=x,y}
  \begin{WHILE}{1}{\stm{\dots}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklketto \\
Ez a feltétel kezünkbe adja a ciklusfeltételt, hiszen $P$ és $R$ összehosonlításából
$\nem\pi$-re $a=b$ adódik (hiszen az $a=b=lnko(a,b)$ csak így teljesülhet).
Tehát $\pi = (a \ne b)$.
\begin{stuki}[6cm]
  \stm{a,b:=x,y}
  \begin{WHILE}{1}{\stm{a \ne b}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklharom \\
Jelen esetben ez: $Q \es a\in [1..x] \es b\in [1..y] \es \lnko(a,b)=\lnko(x,y)\kov t>0$. Tehát $t:=a+b$
egy megfelelő terminálófüggvény.

\cklot \\
Ellenőrízzük, hogy a következő program biztosítja ezt a tulajdonságot:
\begin{stuki*}[6cm]{$S_0$}
  \begin{IF}{1}{\stm{a < b}}
  \stm{b:=b-a}
  \ELSE
  \stm{a:=a-b}
  \end{IF}
\end{stuki*}
5/\elagegy{P\es\pi\es t=t_0}  Ez nyilván teljesül (sőt az is igaz, hogy a teljes állapotteret leírjuk).\\
5/\elagketto{P \es \pi\es t=t_0}{t<t_0}
\vspace{-1cm}
\begin{enumerate}
\item{$a<b$:} $P\es\pi\es a+b=t_0 \kovkerdes\lf(b:=b-a,t<t_0)=a+b-a=b<t_0 \surd (\textrm{hiszen }a>0)$
\item{$a\ge b$:} $P\es\pi\es a+b=t_0 \kovkerdes\lf(a:=a-b,t<t_0)=a-b+b=a<t_0 \surd (\textrm{hiszen }b>0)$
\end{enumerate}
\cklnegy \\
A mi esetünkben:\\
$(Q \es a\in [1..x] \es b\in [1..y] \es \lnko(a,b)=\lnko(x,y) \es a \ne b) \kovkerdes \lf(S_0, P)$

4/\elagegy{P\es\pi}  Ez nyilván teljesül (sőt az is igaz, hogy a teljes állapotteret leírjuk).\\
4/\elagketto{P\es\pi}{P}
\vspace{-1cm}
\begin{enumerate}
\item{$a<b$:} $P\es\pi\es a<b \kovkerdes\lf(b:=b-a,P)$\\
$(Q \es a\in [1..x] \es b\in [1..y] \es \lnko(a,b)=\lnko(x,y) \es a<b)$\\$\kovkerdes$\\
$\lf(b:=b-a, P)=(Q \es a\in [1..x] \es b-a\in [1..y] \es \lnko(a,b-a)=\lnko(x,y)) \surd$
\item{$a\ge b$:} $P\es\pi\es a>b \kovkerdes\lf(a:=a-b,P)$\\
$(Q \es a\in [1..x] \es b\in [1..y] \es \lnko(a,b)=\lnko(x,y) \es a>b)$\\$\kovkerdes$\\
$\lf(a:=a-b, P)=(Q \es a-b\in [1..x] \es b\in [1..y] \es \lnko(a-b,b)=\lnko(x,y)) \surd$
\end{enumerate}

Ezen következések felismeréséhez szükséges az alábbi tétel:\\
$\lnko(a,b)=\lnko(a-b,b) \qquad (\textrm{ha } a>b)$\\
Bizonyítás: \\
Ha egy szám osztója $a$-nak és $b$-nek is, akkor $a-b$-nek is,
illetve, ha osztója $a-b$-nek és $b$-nek, akkor $a$-nak is, ui.:
\begin{enumerate}
\item $\forall x\in \N: (\exists c,d\in\N: cx = a \es dx = b) \overset{a>b}{\kov} (c-d)x = a-b$
\item $\forall x\in \N: (\exists c,d\in\N: cx = a-b \es dx = b) \kov (c+d)x = a$
\end{enumerate}

Ha a közös osztók halmaza pontosan egyenlő (és véges), akkor a
maximális elem (az lnko) is egyezik.  Ezzel a tételt megmutattuk.

\begin{stuki}[6cm]
  \stm{a,b:=x,y}
  \begin{WHILE}{2}{\stm{a \ne b}}
    \begin{IF}{1}{\stm{a < b}}
      \stm{b:=b-a}
      \ELSE
      \stm{a:=a-b}
    \end{IF}
  \end{WHILE}
\end{stuki}

\end{document}