\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 4. feladat, 3. megoldás}
\begin{document}
\noindent
\emph{Feladat:} Határozzuk meg --- a hatványozás műveletének használata nélkül --- az x szám n-edik hatványát!

\emph{Specifikáció:}\\
$A = \alatt{\Z}{x} \times \alatt{\N}{n} \times \alatt{\Z}{r} \times \alatt{\Z}{b} \times \alatt{\Z}{k}$\\
$B = \alatt{\Z}{x'} \times \alatt{\N}{n'}$\\
$Q = ( x=x' \es n=n' \es n \ne 0 )$\\
$R = ( Q \es r=x^n )$

\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 k\in[0..n] \es x^n=r*b^k)$

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 k=n \es b=x \es r=1)$

Látható, hogy $Q' \kov P$ és $Q \kov \lf(k,b,r:=n,x,1 , Q') = Q$.

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{k,b,r:=n,x,1}
  \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 $k=0$ adódik.  Tehát $\pi = (k \ne 0)$.  (Megjegyzés: jelenleg $b=1$-re
is gondolhatnánk, de az nem lenne jó.)
\begin{stuki}
  \stm{k,b,r:=n,x,1}
  \begin{WHILE}{1}{\stm{k \ne 0}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklharom \\
Jelen esetben ez: $Q \es k\in[1..n]\es x^n=r*b^k \kov t>0$. Tehát $t:=k$
egy megfelelő terminálófüggvény.\\
\cklot \\
Előrevéve az utolsó feltételt már most biztosíthatjuk, hogy a programunk lefutása
véges legyen.  Mivel $t=k$, a megoldás csak $k$ csökkentése lehet.
Nézzük az alábbi struktogramot $S_0$-ként:
\begin{stuki}
  \begin{IF}{1}{\stm{2|k}}
    \stm{k,b:=k/2, b*b}
    \ELSE
    \stm{k,r:=k-1, r*b}
  \end{IF}
\end{stuki}
Annak bizonyítását, hogy ez az elágazás mindig csökkenti k értékét, az olvasóra bízom.

\cklnegy \\
Ezen állítás igazolásához az elágazás levezetési szabályának feltételeit kell ellenőríznunk:\\
4/\elagegy{P\es\pi}\\
A fenti formájú egyszerűsített elágazásoknál ez mindig igaz, hiszen a második feltétel
igazából az első pontos negáltja, így az állapottér összes pontjában igaz kettőjük
valamelyike.\\
4/\elagketto{P\es\pi}{P}
\begin{enumerate}
\item $2|k$:\\
$Q\es k\in[1..n]\es x^n=r*b^k \es 2|k \kovkerdes Q\es k/2\in[0..n]\es x^n=r*(b*b)^{k/2} \surd$
\item $\nem (2|k)$:\\
$Q\es k\in[1..n]\es x^n=r*b^k \es \nem (2|k) \kovkerdes Q\es k-1\in[0..n]\es x^n=r*b*b^{k-1} \surd$
\end{enumerate}

Figyeljük meg, hogy ebben a feladatmegoldásban már az 5. pont
megfontolásakor olyan ciklusmagot találtunk (a k növeléséhez), hogy
azt már nem kellett megváltoztatnunk a 4. pont bizonyításakor, mint
egyéb esetekben.  (Természetesen ez nem volt véletlen.)

\begin{stuki}
  \stm{k,b,r:=n,x,1}
  \begin{WHILE}{2}{\stm{k \ne 0}}
  \begin{IF}{1}{\stm{2|k}}
    \stm{k,b:=k/2, b*b}
    \ELSE
    \stm{k,r:=k-1, r*b}
  \end{IF}
  \end{WHILE}
\end{stuki}

\end{document}