\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, faktoriális}
\begin{document}
\noindent

\emph{Feladat}\\Határozzuk meg az $n!=1\cdot2\cdots n$ értékét!

\emph{Specifikáció:}\\
$A = \alatt{\N_0}{n} \times \alatt{\N}{r}$\\
$B = \alatt{\Z}{n'}$\\
$Q = ( n=n' )$\\
$R = ( Q \es r=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 (és új állapottere)?

$A' = \alatt{\N_0}{n} \times \alatt{\N}{r} \times \alatt{\N_0}{k}$\\
$P  = (Q \es k\in [0..n] \es r=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=0 \es r=1 )$

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

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{k,r:=0,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=n$ adódik.  Tehát $\pi = (k \ne n)$.

\cklharom\\
Jelen esetben ez: $Q \es k\in[0..n-1] \es r=k! \kov t>0$. Tehát $t:=n-k$
egy megfelelő terminálófüggvény.

\cklnegyot\\

A ciklusmagban $k$ értékét biztos növeljük, viszont az invariánst is
meg kell tartanunk, ezt teszi egyszerre a $k,r:=k+1,r(k+1)$ szimultán
értékadás, lássuk mi ennek a leggyengébb előfeltétele a $P \es
t=t_0$-ra vonatkozóan: $\lf(k,r:=k+1,r(k+1), P \es n-k=t_0) = ( Q \es
k+1\in [0..n] \es r(k+1)=(k+1)! \es n-k-1 = t_0 )$.  Ez a feltétel
azonban következik $P \es \pi \es t=t_0$-ból.

\begin{stuki}[6cm]
  \stm{k,r:=0,1}
  \begin{WHILE}{1}{\stm{k \ne n}}
    \stm{k,r:=k+1,r(k+1)}
  \end{WHILE}
\end{stuki}
\end{document}