\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 81. feladat}
\begin{document}
\noindent
\emph{Feladat:} Egy múzeumba az $i$-dik órában $x(i)$ látogató érkezik,
és $y(i)$ látogató megy el.  Melyik órában volt a legtöbb látogató a
múzeumban?

\emph{Átfogalmazás:} \\
$\phi:[a,b]\nyil \N_0$\\
$\phi(a) = x(a)$, 
$\forall i\in [a+1,b]: \phi(i) = F(i, \phi(i-1))$, ahol 
$F: [a+1,b] \times \N \nyil \N$ definíciója: $F(i, z):=z+x(i)-y(i)$.

Vegyük észre, hogy éltünk azzal a feltételezéssel, hogy a múzeumban
a nap elején nincsenek látogatók, valamint feltettük azt is, hogy az
$x$, $y$ függvények értelmesen vannak megadva és így a múzeumban sosem
lesz negatív számú látogató.

Ezzel a $\phi$ függvénnyel a feladat a maximum keresésre vezethető
vissza.

\emph{Specifikáció:}\\
$A = \alatt{\N}{a} \times \alatt{\N}{b} \times \alatt{\N}{i}$\\
$B = \alatt{\N}{a'} \times \alatt{\N}{b'}$\\
$Q = ( a=a' \es b=b' \es a\le b )$\\
$R = ( Q \es i\in[a,b] \es \forall j\in[a,b]:\phi(j)\le\phi(i))$

A visszavezetés alteres általánosított, hiszen a $max$ értékre kikötést
nem specifikáltunk.

\begin{tabular}{ccc}
feladat &  & max. ker \\
\hline
$a$ & \knyil & $m$ \\
$b$ & \knyil & $n$ \\
$\phi(i)$ & \knyil & $f(i)$
\end{tabular}

\begin{stuki}[8cm]
  \stm{i,k,max:=a,a,\phi(a)}
  \begin{WHILE}{3}{\stm{k \ne b}}
    \begin{CASE}{1}{2}
      \WHEN{\stm{\phi(k+1)\ge max}}
      \stm{i,max:=k+1,\phi(k+1)}
      \WHEN{\stm{\phi(k+1)\le max}}
      \SKIP
    \end{CASE}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

Felhasználva a rekurzív függvény változóval való helyettesítésének
programtranszformációs módszerét $\phi$-re:

\begin{stuki}[6cm]
  \stm{i,k,max:=a,a,x(a)}
  \begin{WHILE}{4}{\stm{k \ne b}}
    \stm{z:=z+x(k+1)-y(k+1)}
    \begin{IF}{1}{\stm{z>max}}
      \stm{i,max:=k+1,z}
      \ELSE
      \SKIP
    \end{IF}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
\end{document}