\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 4. feladat, 1. 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.  Próbáljuk a feladatot úgy megoldani, hogy csak eggyel növeljük.
\begin{stuki*}{$S_0$}
  \stm{k:=k+1}
\end{stuki*}
$P\es\pi\es t=t_0 \kov t=t_0 \ekv n-k=t_0 \kovkerdes\lf(S_0, n-k<t_0)=n-k-1<t_0 \surd$

\cklnegy \\
A mi esetünkben:\\
$Q \es k\in[1..n-1]\es r=x^k \kovkerdes Q \es k+1\in[1..n]\es r=x^{k+1}=x*x^k$

Látható, hogy ez a feltétel nem teljesül, ha $x\ne 0$. \\
Azonban kiszámoltuk $\lf(S_0, P)$-t, ezt az eredményt ne hagyjuk veszni, hanem
nevezzük el $Q''$-nek és próbáljunk meg eljutni ide egy másik programrészlettel!
Ha sikerrel járunk, akkor a szekvencia levezetési szabályát alkalmazva rögtön
megkapjuk a feltételt kielégítő ciklusmagot.  Fontos, hogy miközben az előbb
említett részprogramot keressük, olyanok szóba sem jöhetnek, amik $k$ értékét 
megváltoztatják, hiszen ezek elrontanák a már bizonyított 5. követelményt.

A megoldás természetesen egy értékadás lesz, aminek tehát a $P\es\pi\kov\lf(S_{01}, Q'')$
követelményt kell teljesítenie.
\begin{stuki*}{$S_{01}$}
  \stm{r:=x*r}
\end{stuki*}

$Q \es k\in [1..n-1] \es r=x^k \kovkerdes \lf(r:=x*r, Q'')= Q \es k+1\in[1..n]\es x*r=x*x^k\surd$

\begin{stuki}
  \stm{k,r:=1,x}
  \begin{WHILE}{2}{\stm{k \ne n}}
    \stm{r:=x*r}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

\end{document}