\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{3. feladatsor, 10. feladat}
\begin{document}
\noindent
\emph{Feladat:} Az $x$ szekvenciális file egész számokat tartalmaz
(megengedett művelet az $sx,dx,x$:read).  Keressünk a file-ban lokális
maximumot, vagyis olyan értéket, ami mindkét közvetlen szomszédjánál
nagyobb!

A feladat megoldása adott file helyett $f$ függvény esetén egy
egyszerű lin. ker. 2.8-ra való visszavezetés lenne, ahol a
$\beta(i)=(f(i-1)<f(i)>f(i+1))$.  Gondolhatnánk, hogy a szokásos
átírási szabályainkkal ebből tudunk file-on működő verziót csinálni,
de a problémát az okozza, hogy a sorozatra való átírás csak olyan
programmal tud boldogulni, ami a ciklusukban $f$-nek csak $i+1$
indexű elemére hivatkozik.

Egy rekurzív függvény segítségével tudunk adni olyan megoldást, ami $f$-nek mindig csak az $i+1$-edik elemét használja:\\
$\varphi\colon[m+1,n]\nyil\Z\times\Z\times\Z$\\
$\varphi(m+1):=(0,f(m),f(m+1))$\\
$\forall i\in[m+2,n]: \varphi(i) := F(i, \varphi(i-1))$, ahol $F(i,z):=(z.2, z.3, f(i))$

Ennek a $\varphi$ függvénynek keressük egy olyan elemét, ahol a középső komponens a legnagyobb.

\emph{Specifikáció:}\\
$A = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\L}{l}$\\
$B = \alatt{\Z}{m'} \times \alatt{\Z}{n'}$\\
$Q = ( m=m' \es n=n' \es m\le n-1 )$\\
$R = ( Q \es l=(\exists i\in [m+2,n]: \varphi(i).1<\varphi(i).2>\varphi(i).3))$

Alkalmazzuk a rekurzív függvény változóval való helyettesítésének programtranszformációs módszerét:
\begin{stuki}[6cm]
  \stm{i,l:=m+1, \hamis}
  \stm{z:=(0, f(m), f(m+1))}
  \begin{WHILE}{3}{\stm{\nem l \es i \ne n}}
    \stm{z:=(z.2, z.3, f(i+1))}
    \stm{l:=(z.1<z.2>z.3)}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

Ezt a stukit már könnyű átírni fájlokra:
\begin{stuki}[6cm]
  \stm{sx,dx,x:\Read}
  \stm{z_2:=dx}
  \stm{sx,dx,x:\Read}
  \stm{z_3:=dx}
  \stm{l,z:=\hamis,(0,z_2,z_3)}
  \stm{sx,dx,x:\Read}
  \begin{WHILE}{3}{\stm{sx=norm}}
    \stm{z:=(z.2, z.3, f(i+1))}
    \stm{l:=(z.1<z.2>z.3)}
    \stm{sx,dx,x:\Read}
  \end{WHILE}
\end{stuki}
\end{document}