\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 16. feladat}
\begin{document}
\noindent
\emph{Feladat:} Az $x$ egész számokból álló vektor egy decimális szám számjegyeit
tartalmazza helyiérték szerint csökkenő sorrendben.  Számítsuk ki az ábrázolt szám
értékét!

$\V = \vect(\Z, \{0, 1, \cdots, 9\})$

A feladat megoldása során használni fogjuk a következő két függvényt:\\
$f(x)::=\sum\limits_{i=0}^{x.dom-1} x_{x.hib-i} * 10^i \hspace{1cm} (\forall x \in \V)$\\
$g(x,l)::=\sum\limits_{i=0}^{l-1} x_{x.lob+l-i-1} * 10^i \hspace{1cm} (\forall x \in \V: \forall l\in[0,x.dom])$

Az $f$ függvény egy vektorban ábrázolt szám értékét számítja ki, míg
$g$ ugyanezt teszi, de csak az első $l$ számjegyet veszi figyelembe.
Vegyük észre, hogy $g(x, x.dom) = f(x)$.

\emph{Specifikáció:}\\
$A = \alatt{\V}{x} \times \alatt{\N_0}{d}$\\
$B = \alatt{\V}{x'}$\\
$Q = (x=x')$\\
$R = ( Q \es d=f(x))$

\emph{Megoldás:}\\
$P = ( Q \es k\in[0,x.dom] \es d=g(x, k))$\\
$Q' = (Q \es k=0 \es d=0)$

Ellenőrízzük le a ciklus feltételeit:\\
\cklegy \\
$Q \kov \lf(k,d:=0,0, Q') = Q$.

\cklketto \\
$P$ és $R$ összehosonlításából $\nem\pi$-re $k=x.dom$ adódik.  Tehát $\pi = (k\ne x.dom)$.
\begin{stuki}
  \stm{k,d:=0,0}
  \begin{WHILE}{1}{\stm{k\ne x.dom}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}

\cklharom \\
$t:=x.dom-k$ választással ez az állítás triviálisan teljesül.

\cklnegyot \\
Egy szekvenciával, aminek közbülső feltétele:\\
$Q'' = ( \lf(k:=k+1, P) \es t=t_0 ) = ( Q \es k+1 \in[0,x.dom] \es d=g(x, k+1) \es t=t_0)$

Ez azért jó választás, mert ebből az állapotból a $k:=k+1$ utasítással
eljuthatunk $P \es t<t_0$-ba.

A szekvencia levezetési szabálya szerint szükséges $P\es\pi\es t=t_0 \kov \lf(S_1, Q'')$
állítást pedig az $S_1 = (d:=d*10+x_{x.lob+k})$ programmal teljesíthetjük, hiszen:\\
$(P\es\pi\es t=t_0) = (Q \es k\in[0,x.dom-1] \es d=g(x, k) \es t=t_0)$ \\
$\kovkerdes \lf(S_1, Q'')=(Q \es k+1 \in[0,x.dom] \es d*10+x_{x.lob+k}=g(x, k+1) \es t=t_0) \surd$.

Ugyanis, $g(x,k)*10+x_{x.lob+k} = (\sum\limits_{i=0}^{k-1} x_{x.lob+k-i-1} * 10^i)*10 + x_{x.lob+k} =
(\sum\limits_{i=1}^{k} x_{x.lob+k-i} * 10^{i-1})*10 + x_{x.lob+k}*10^0 = (\sum\limits_{i=0}^{k} x_{x.lob+k-i} * 10^i)=
g(x, k+1)$.
\begin{stuki}[8cm]
  \stm{k,d:=0,0}
  \begin{WHILE}{2}{\stm{k\ne x.dom}}
    \stm{d:=d*10+x_{x.lob+k}}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
\end{document}