\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 3. feladat}
\begin{document}
\noindent
\emph{Feladat:} Határozzuk meg az $x$ és az $y$ természetes számok legkisebb
közös többszörösé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=\lkkt(x,y))$

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

\emph{Megoldás:}\\
A specifikációnak megfelelő megoldó program egy szekvenciából fog állni, aminek első
fele a már ismertetett legkisebb közös osztó számító algoritmus (2. feladat). Ennek utófeltételét
nevezzük $R'$-nek:\\
$R' = ( Q \es a=b=\lnko(x,y))$

Nézzük most a szekvencia levezetési szabályát:\\
$( Q\kov \lf(S_0, R') \es R'\kov \lf(S_1, R) ) \kov (Q\kov \lf((S_0;S_1),R))$

A feltétel rész első felét a 2. feladat bizonyítása igazolja, tehát mi csak
$R'\kov \lf(S_1, R)$ állítást bizonyítjuk $S_1:=(a:=\frac{xy}{a})$ programra.

$R'\kovkerdes \lf(S_1, R) = (Q \es \frac{xy}{a}=\lkkt(x,y))$, ahol $a=\lnko(x,y)$
(figyelembe véve $R'$-t).  Tehát a jól ismert tételre ($\lkkt(x,y) =
\frac{xy}{\lnko(x,y)}$) jutottunk.

\begin{stuki}
  \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}
  \stm{a:=\frac{xy}{a}}
\end{stuki}

\end{document}