% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 76. feladat}
\begin{document}
\noindent
\emph{Feladat:} Állapítsuk meg, hogy az $x$ szám binárisan felírt
alakjában hány darab 1-es szerepel!

\def\div{\text{ div }}

\emph{Specifikáció:}\\
$A = \alatt{\N}{x} \times \alatt{\No}{i}$\\
$B = \alatt{\N}{x'}$\\
$Q = ( x=x' )$\\
$R = ( Q \es i\ge 0 \es f(i)_1=0)$, ahol
\begin{align*}
f&\colon[-1, 0] \cup \N\to\N\times\No \\
f(-1)&:=(x,0) \\
\forall i\ge0&\colon f(i):=F(i, f(i-1)) \\
F(k,z)&:=(z_1 \div2, z_2+(z_1 \bmod 2))
\end{align*}

$R \kov (f(i)_2=\sum\limits_{i=0}^\infty\chi(f(i) \bmod 2)=1)$, így,
ha egy olyan $f(i)$ értéket kiszámolunk a programban, ahol $f(i)_1
=0$, akkor ott a kiszámolt érték második komponense pont a kívánt
végeredményt fogja adni.

Visszavezetés a lin. ker. 2-re, hiszen $f(i)_1=0$ előbb-utóbb igaz.
Az $x$ a visszavezetés paramétere, az $m$-et a 0 konstanssal helyettesítjük.

\begin{tabular}{ccc}
  feladat &  & lin. ker. 2 \\
  \hline
  $0$ & \knyil & $m$ \\
  $f(j)_1 = 0$ & \knyil & $\beta(j)$
\end{tabular}

\begin{stuki}[7cm]
  \stm{l,k:=\hamis,-1}
  \begin{WHILE}{2}{\stm{\nem l}}
    \stm{l:=f(k+1)_1 =0}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

Az $f$ függvény rekurzívan definiált, ezért alkalmazhatjuk a
rekurzívan definiált függvény változóval való helyettesítésének
programtranszformációs módszerét, amivel kapjuk a nem megengedett
értékadást már nem tartalmazó végeredmény programot:

\begin{stuki}[7cm]
  \stm{z,e,l,k:=x,0, \hamis,-1}
  \begin{WHILE}{3}{\stm{\nem l}}
    \stm{z,e:=z\div2, e+(z \bmod 2)}
    \stm{l:=(z=0)}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

A programban $k$ csak az értékadások bal oldalán szerepel, így szükségtelen:
\begin{stuki}[7cm]
  \stm{z,e,l:=x,0, \hamis}
  \begin{WHILE}{2}{\stm{\nem l}}
    \stm{z,e:=z\div2, e+(z \bmod 2)}
    \stm{l:=(z=0)}
  \end{WHILE}
\end{stuki}

\end{document}