% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 5. feladat}
\begin{document}
\noindent
\emph{Feladat:} Döntsük el, hogy a $k$ természetes szám osztja-e az $x$ természetes számot!

\emph{Specifikáció:}\\
$A = \alatt{\N}{x} \times \alatt{\N}{k} \times \alatt{\L}{l}$\\
$B = \alatt{\N}{x'} \times \alatt{\N}{k'}$\\
$Q = ( x=x' \es k=k' )$\\
$R = ( k=k' \es l=k'|x' )$

Vegyük észre, hogy az utófeltételbe ezúttal nem írtuk be $Q$-t.  Ennek
az az oka, hogy speciálisan most meg akarjuk engedni azt, hogy $x$
értékét a program a futása során változtassa.  Fontos, hogy az
oszhatóságot természetesen az eredeti $k'$-re és $x'$-re specifikáljuk
(és $k=k'$-t kikössük), különben az egyszerű $l,x,k:=\igaz,1,1$
értékadás megoldaná a feladatot.  Tulajdonképpen, ha ez valakinek nem
szimpatikus, akkor egy segédváltozó használatával ezt a furcsaságot
megszüntetheti.

\emph{Megoldás:}\\
Először írjunk egy olyan programot, ami csak a következő utófeltételt
teljesíti: $R' = ( k=k' \es x\le k \es k|x \knyil k|x' )$, azaz $x$ értékét
legalább $k$-ig csökkenti, úgy, hogy az oszthatóság tényén az eredeti
$x'$-höz képest nem változtat.  Ebből az $R'$ állapotból egy egyszerű
elágazással elérhetjük $R$ állapotot, mivel ha $R'$-höz hozzávesszük
még $x=k$-t, akkor pont $k'|x'$ állítást kapjuk, ha pedig $x\ne k$-t,
akkor $\nem(k'|x')$ állítást.  Azaz az előbbi esetben $l$-et igazra,
az utóbbi esetben $l$-et hamisra állíthatjuk.  Az egész program tehát
egy szekvenciából fog állni, aminek közbülső feltétele $R'$, és a
szekvencia második programja az alábbi elágazás:
\begin{stuki*}[6cm]{$S_2$}
  \begin{IF}{1}{\stm{x=k}}
    \stm{l:=\igaz}
    \ELSE
    \stm{l:=\hamis}
  \end{IF}
\end{stuki*}

Az elágazás levezetési szabályának első pontja triviálisan teljesül.

A második pont:
\elagketto{R'}{R}
\begin{enumerate}
\item $x=k$:\\
$k=k' \es x=k \es k|x \knyil k|x' \kovkerdes k=k' \es \igaz=k'|x' \surd$
\item $x \ne k$:\\
$k=k' \es x<k \es k|x \knyil k|x' \kovkerdes k=k' \es \hamis=k'|x' \surd$
\end{enumerate}

Azaz $R' \kov lf(S_2, R)$, ami a szekvencia levezetési szabályának második pontja.

Most keressük meg azt az $S_1$ programot, amire $Q\kov lf(S_1, R')$ és
így teljesíti a szekvencia levezetési szabályának az első pontját!

Ez a program egy ciklus lesz, a következő invariánssal:

$P = (k=k' \es k|x \knyil k|x' )$

Ellenőrízzük le a ciklus feltételeit:\\
\cklegy \\
Teljesül, hiszen az ekvivalencia nyíl két oldala $x=x'$ mellett ugyanaz.

\cklketto \hspace{-2mm} $'$ \\
Ez a feltétel kezünkbe adja a ciklusfeltételt, hiszen $P$ és $R'$ összehosonlításából
$\nem\pi$-re $x\le k$ adódik.  Tehát $\pi = (x > k)$.

\cklharom \\
Jelen esetben ez: $k=k' \es k|x \knyil k|x' \es x > k$. Tehát $t:=x$
egy megfelelő terminálófüggvény.

\cklnegyot \\
\begin{stuki*}[6cm]{$S_0$}
  \stm{x:=x-k}
\end{stuki*}

$S_0$ valóban jó ciklusmag:

$k=k' \es k|x \knyil k|x' \es x > k \es t_0=x \kovkerdes k=k' \es k|x-k \knyil k|x' \es x-k < t_0 \surd$

Ezzel a ciklust levezettük és így tudjuk, hogy az $S_1$ ciklusra: $Q\kov lf(S_1, R')$

\begin{stuki*}[6cm]{$S_1$}
  \begin{WHILE}{1}{\stm{x>k}}
    \stm{x:=x-k}
  \end{WHILE}
\end{stuki*}

A feladat végleges megoldása:
\begin{stuki*}[6cm]{$S$}
  \begin{WHILE}{1}{\stm{x>k}}
    \stm{x:=x-k}
  \end{WHILE}
  \begin{IF}{1}{\stm{x=k}}
    \stm{l:=\igaz}
    \ELSE
    \stm{l:=\hamis}
  \end{IF}
\end{stuki*}

\end{document}