\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 4. feladat, 2. 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}{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[1..n] \es r=x^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=1 \es r=x)$

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

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{k,r:=1,x}
  \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=n$ adódik.  Tehát $\pi = (k \ne n)$.
\begin{stuki}
  \stm{k,r:=1,x}
  \begin{WHILE}{1}{\stm{k \ne n}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklharom \\
Jelen esetben ez: $Q \es k\in[1..n-1]\es r=x^k \kov t>0$. Tehát $t:=n-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=n-k$ és $n$ az invariáns szerint nem változhat, a megoldás
csak $k$ növelése lehet.  Most a szokásostól eltérően, megpróbáljuk $k$-t
drasztikusabb mértékben növelni.\\
Nézzük az alábbi struktogramot $S_0$-ként:
\begin{stuki}
  \begin{IF}{1}{\stm{2*k\le n}}
    \stm{k,r:=2*k, r*r}
    \ELSE
    \stm{k,r:=k+1, r*x}
  \end{IF}
\end{stuki}
Annak bizonyítását, hogy ez az elágazás mindig növeli 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 $k*2\le n$:\\
$Q\es k\in[1..n-1]\es r=x^k \es k*2\le n \kovkerdes Q\es 2*k\in[1..n]\es r*r=x^{2*k}=x^k*x^k \surd$
\item $k*2 > n$:\\
$Q\es k\in[1..n-1]\es r=x^k \es k*2>n \kovkerdes Q\es k+1\in[1..n]\es r*x=x^{k+1}=x^k*x \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,r:=1,x}
  \begin{WHILE}{2}{\stm{k \ne n}}
    \begin{IF}{1}{\stm{2*k\le n}}
      \stm{k,r:=2*k, r*r}
      \ELSE
      \stm{k,r:=k+1, r*x}
    \end{IF}
  \end{WHILE}
\end{stuki}

\end{document}