\input menv
\input stuki

\newdimen\conspace\conspace=2pt
\newdimen\spspace\spspace=4pt
\def\con#1{\vskip\conspace\item{}#1\vskip\conspace}
\def\conp#1#2{\vskip\conspace\item{#1}#2\vskip\conspace}

\newcount\spsw\spsw=0
\def\var(#1:#2){\ifodd\spsw{$\times $}\else{\global\spsw=1}\fi
            {\baselineskip 9pt\vtop{\hbox{#1}\hbox{$#2$}}}}
\def\sp#1{\vskip\spspace\global\spsw=0\item{}$#1=$}
\def\edef{\mathrel{\mathop=^{{\fiverm def}}}}

\font\kiscimf=cmbx10
\font\kiemf=cmssqi8
\newcount\tetelc\tetelc=0
\newcount\altetelc\altetelc=0
\newcount\alaltetelc\alaltetelc=0
\def\tetel#1{\advance\tetelc by 1 \altetelc = 0 \alaltetelc = 0
             \vskip 2mm
             \leftline{{\kiscimf\number \tetelc .\enskip #1}}
             \vskip 1.2 mm}

\def\altetel#1{\advance\altetelc by 1 \alaltetelc = 0
               \vskip 1.2mm
               \leftline{{\kiscimf\number\tetelc .\number\altetelc .\enskip #1}}
               \vskip 1.2mm}

\def\alaltetel#1{\advance\alaltetelc by 1
                 \vskip .8mm
                 \leftline{{\kiscimf\number\tetelc .\number\altetelc .\number\alaltetelc .\enskip #1}}
                 \vskip 1.2mm}


% ---- [m..n] u { m - 1 } ----
\def\mn{ [ m .. n ] \cup \{ m - 1 \} }

{\bf A feladat specifik\'aci\'oja:}
\bigskip
Legyen $\X:vekt(\N,\{0,1,2,...,9\})$.

\sp{A}\var(\No:n)\var(\N:s)\var(\X:x)
\sp{B}\var(\N:{n^\prime})
\medskip

\con{$Q:\bigl(n=n^\prime \bigr)$}
\con{$R:\bigl(n'=\sum\limits_{j=x.lob}^{x.hib}x[j]\cdot 10^{(x.hib-j)}
               \land s=szjsz(n') \ \land n'=x.dom
 \bigr)$}
\medskip

Keress\"uk a megold\'ast ad\'o programot {\bf ciklus} form\'aban, ahol

\con{$P:\bigl(s\in [0..x.dom]\land \ n'=x.dom\ \land
\nl
        \land\ n'=(\sum\limits_{x.hib-s+1}^{x.hib}x[j]\cdot 10^{(x.hib-j)}) + n\cdot 10^s
        \land \forall j\in[x.lob..x.hib-s]:x[j]=0 \land
\nl
        \land\ n>0 \rightarrow szjsz(n') = szjsz(n) + s
        \land\ n=0 \rightarrow szjsz(n') = s
\bigr)$}
\bigskip

\itemitem{1.}$Q\not\Rightarrow P$, de $Q\Rightarrow P^{s,x\leftarrow 0,(1,<0_1,0_2,....,0_n>)}$.
\nl
Innen ad\'odik, hogy
\nl
$Q\Rightarrow\lf(s,x := 0,(1,<0_1,0_2,....,0_n>),\ P)$
\itemitem{2.} A ciklus levezet\'esi szab\'alya m\'asodik felt\'etele:
\hfill\break
$P\land\neg\pi \Rightarrow R$
\hfill\break
teljes\"ul, ha $\neg\pi:\ (n = 0)$.
\nl
Ez\'ert $\pi:\ (n > 0)$ alkalmas v\'alaszt\'as.
\itemitem{3.} A ciklus levezet\'esi szab\'alya harmadik felt\'etele:
\hfill\break
$P\land\pi \Rightarrow t > 0$
\hfill\break
teljes\"ul, ha $t:\ n$
\hfill\break
a $\pi$ v\'alaszt\'asa miatt.
\itemitem{4.} \'es 5. Bel\'athat\'o, hogy
\hfill\break
$P\land n>0 \Rightarrow
\bigl((s+1) \in [0..x.dom]\land\ n'=x.dom\ \land
\nl
        \land\ n'=(n\ mod\ 10)\cdot 10^s + (\sum\limits_{x.hib-s+1}^{x.hib}x[j]\cdot 10^{(x.hib-j)}) + (n\ div\ 10)\cdot 10^{(s+1)}\ \land
\nl
        \land\ \forall j\in[x.lob..x.hib-(s+1)]:x[j]=0 \land
\nl
        \land\ (n\ div\ 10) >0 \rightarrow szjsz(n') = szjsz((n\ div\ 10)) + (s+1)\ \land
\nl
        \land\ (n\ div\ 10) =0 \rightarrow szjsz(n') = (s+1)
\bigr)$
\hfill\break
ez\'ert
\hfill\break
$P\land\pi \Rightarrow P^{n,s,x[x.hib-s] \leftarrow (n\ div\ 10), s+1, (n\ mod\ 10)})$
\hfill\break
Innen ad\'odik, hogy
\hfill\break
$P\land\pi \Rightarrow\lf(n,s,x[x.hib-s] := (n\ div\ 10), s+1, (n\ mod\ 10),\ P)$
\bigskip

Egy lehets\'eges megold\'as teh\'at a k\"ovetkez\H o program:

\smallskip
\Stuki{} 250pt :
    \Stm $s,x := 0,(1,<0_1,0_2,....,0_n>) $;
    \Rule
    \WHILE \Stm $n > 0 $; DO
        \Stm $n,s,x[x.hib-s] := (n\ div\ 10), s+1, (n\ mod\ 10) $;
    \ENDDO
\END.


\bigskip

Legyen $\X:fun(\N,\{0,1,2,...,9\})$.

\sp{A}\var(\No:n)\var(\N:s)\var(\X:x)
\sp{B}\var(\N:{n^\prime})
\medskip

\con{$Q:\bigl(n=n^\prime \bigr)$}
\con{$R:\bigl(n'=\sum\limits_{j=x.lob}^{x.hib}x[j]\cdot 10^{(x.hib-j)}
               \land\ x[x.lob] \ne 0\ \land s=szjsz(n')
 \bigr)$}
\medskip

Keress\"uk a megold\'ast ad\'o programot {\bf ciklus} form\'aban, ahol

\con{$P:\bigl(
               n'=(\sum\limits_{x.lob}^{x.hib}x[j]\cdot 10^{(x.hib-j)}) + n\cdot 10^{(x.hib-x.lob+1)}
        \land  s = x.hib-x.lob+1 \land
\nl
        \land\ n>0 \rightarrow szjsz(n') = szjsz(n) + s
        \land\ n=0 \rightarrow szjsz(n') = s
\bigr)$}
\bigskip

\itemitem{1.}$Q\not\Rightarrow P$, de $Q\Rightarrow P^{s,x\leftarrow 0,(n,<>)}$.
\nl
Innen ad\'odik, hogy
\nl
$Q\Rightarrow\lf(s,x := 0,(n,<>),\ P)$
\itemitem{2.} A ciklus levezet\'esi szab\'alya m\'asodik felt\'etele:
\hfill\break
$P\land\neg\pi \Rightarrow R$
\hfill\break
teljes\"ul, ha $\neg\pi:\ (n = 0)$.
\nl
Ez\'ert $\pi:\ (n > 0)$ alkalmas v\'alaszt\'as.
\itemitem{3.} A ciklus levezet\'esi szab\'alya harmadik felt\'etele:
\hfill\break
$P\land\pi \Rightarrow t > 0$
\hfill\break
teljes\"ul, ha $t:\ n$
\hfill\break
a $\pi$ v\'alaszt\'asa miatt.
\itemitem{4.} \'es 5. Bel\'athat\'o, hogy
\hfill\break
$P\land n>0 \Rightarrow
\nl
\bigl(
       n'=(n\ mod\ 10)\cdot 10^{(x.hib-(x.lob-1))} + (\sum\limits_{x.lob}^{x.hib}x[j]\cdot 10^{(x.hib-j)}) +
\nl
       +\ (n\ div\ 10)\cdot 10^{(x.hib-(x.lob-1)+1)}\ \land
\nl
        \land\ (s+1)= x.hib-(x.lob-1)+1=0 \land
\nl
        \land\ (n\ div\ 10) >0 \rightarrow szjsz(n') = szjsz((n\ div\ 10)) + (s+1)\ \land
\nl
        \land\ (n\ div\ 10) =0 \rightarrow szjsz(n') = (s+1)
\bigr)$
\hfill\break
ez\'ert
\hfill\break
$P\land\pi \Rightarrow P^{n,s,x \leftarrow (n\ div\ 10), s+1, x:loext((n\ mod\ 10))})$
\hfill\break
Innen ad\'odik, hogy
\hfill\break
$P\land\pi \Rightarrow\lf(n,s,x := (n\ div\ 10), s+1, x:loext((n\ mod\ 10)),\ P)$
\bigskip

Egy lehets\'eges megold\'as teh\'at a k\"ovetkez\H o program:

\smallskip
\Stuki{} 250pt :
    \Stm $s,x := 0,(n,<>) $;
    \Rule
    \WHILE \Stm $n > 0 $; DO
        \Stm $n,s,x := (n\ div\ 10), s+1, x:loext((n\ mod\ 10)) $;
    \ENDDO
\END.



\end
