\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 1. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adott egy $f: \Z \to \Z$ függvény.  Határozzuk meg,
hogy a függvény melyik két pontban veszi fel a maximumát és a minimumát az $[m .. n]$ intervallumon.

\emph{Specifikáció:}\\
$A = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\Z}{k} \times \alatt{\Z}{b}$\\
$B = \alatt{\Z}{m'} \times \alatt{\Z}{n'}$\\
$Q = ( m=m' \es n=n' \es m \le n )$\\
$R = ( Q \es b\in [m..n] \es k\in [m..n] \es \forall i\in [m..n]:f(i)\ge f(k) \es \forall i\in[m..n]:f(i)\le f(b))$

A specifikációból kiolvasható, hogy nem engedjük meg az üres intervallumon
való futtatást, illetve az eredményt az állapottér két változója ($b$ és $k$,
jelentése rendre legnagyobb, legkisebb index) szolgáltatja.

\emph{Megoldás:}\\
Most keressük meg a specifikációnak megfelelő megoldó programot! A megoldást
úgy sejtjük, hogy egy ciklussal találhatjuk meg.  Nos, mi legyen ennek a
ciklusnak az invariánsa (és új állapottere)?

$A'  = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\Z}{k} \times \alatt{\Z}{b} \times \alatt{\Z}{ke} \times \alatt{\Z}{be} \times \alatt{\Z}{i}$\\
$P  = (Q \es b\in [m..n] \es k\in [m..n] \es i\in[m..n] \es f(k)=ke \es f(b)=be \es \forall j\in [m..i]:(f(j)\ge ke \es f(j)\le be) \es ke\le be)$

Ellenőrízzük le a ciklus feltételeit:\\
\cklegy \\
Jól láthatóan nem teljesül, sőt fordítva igaz.  Ezért megpróbálunk egy olyan
közbülső állapotot felírni, ami a $Q$-ból könnyedén (egy értékadással) elérhető és
ugyanakkor ez a kívánt feltétel teljesül rá.  Amennyiben ez sikerül, akkor már csak egy
szekvencia közbülső feltételeként kell pillantani erre az új $Q'$ feltételre
és máris felírható lesz a kívánt program egy értékadás és egy ciklus szekvenciájaként.

$Q' = (Q \es k=m \es b=m \es i=m \es ke=f(k) \es be=f(b))$

Látható, hogy $Q' \kov P$ és $Q \kov \lf(i,b,k,be,ke:=m,m,m,f(m),f(m) , Q') = Q \es m=m \es m=m
\es m=m \es f(m)=f(m) \es f(m)=f(m) = Q$.

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{i,b,k,be,ke:=m,m,m,f(m),f(m)}
  \begin{WHILE}{1}{\stm{\dots}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklketto \\
Ez a feltétel kezünkbe adja a ciklusfeltételt, hiszen $P$ és $R$ összehosonlításából
$\nem\pi$-re $i=n$ adódik.  Tehát $\pi = (i \ne n)$.
\begin{stuki}
  \stm{i,b,k,be,ke:=m,m,m,f(m),f(m)}
  \begin{WHILE}{1}{\stm{i \ne n}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklharom \\
Jelen esetben ez: $Q \es \dots \es i\in[m..n-1]\es\dots\kov t>0$. Tehát $t:=n-i$
egy megfelelő terminálófüggvény.

\cklot \\
Előrevéve az utolsó feltételt már most biztosíthatjuk, hogy a programunk lefutása
véges legyen.  Mivel $t=n-i$ és $n$ az invariáns szerint nem változhat, a megoldás
csak $i$ növelése lehet.  Előretekintve kis gondolkodással látható, hogy egynél
többel nem érdemes növelni.
\begin{stuki*}{$S_0$}
  \stm{i:=i+1}
\end{stuki*}
$P\es\pi\es t=t_0 \kov t=t_0 \ekv n-i=t_0 \kovkerdes\lf(S_0, t<t_0)=n-i-1<t_0 \surd$

\cklnegy \\
A mi esetünkben:\\
$(Q \es b\in [m..n] \es k\in [m..n] \es i\in[m..n-1] \es f(k)=ke \es f(b)=be \es \forall j\in [m..i]:(f(j)\ge ke \es f(j)\le be) \es ke\le be)$\\
$\kovkerdes$\\
$(Q \es b\in [m..n] \es k\in [m..n] \es i+1\in[m..n] \es f(k)=ke \es f(b)=be \es \forall j\in [m..i+1]:(f(j)\ge ke \es f(j)\le be) \es ke\le be)$\\
Látható, hogy ez a feltétel nem teljesül, ha $f(i+1)<ke \vagy f(i+1)>be$. \\
Azonban kiszámoltuk $\lf(S_0, P)$-t, ezt az eredményt ne hagyjuk veszni, hanem
nevezzük el $Q''$-nek és próbáljunk meg eljutni ide egy másik programrészlettel!
Ha sikerrel járunk, akkor a szekvencia levezetési szabályát alkalmazva rögtön
megkapjuk a feltételt kielégítő ciklusmagot.  Fontos, hogy miközben az előbb
említett részprogramot keressük, olyanok szóba sem jöhetnek, amik $i$ értékét 
megváltoztatják, hiszen ezek elrontanák a már bizonyított 5. követelményt.

A megoldás természetesen egy elágazás lesz, aminek tehát a $P\es\pi\kov\lf(S_{01}, Q'')$
követelményt kell teljesítenie.
\begin{stuki*}{$S_{01}$}
  \begin{CASE}{1}{3}
    \WHEN{\stm{f(i+1)\le ke}}
    \stm{k,ke:=i+1,f(i+1)}
    \WHEN{\stm{f(i+1)\ge be}}
    \stm{b,be:=i+1,f(i+1)}
    \WHEN{\stm{ke\le f(i+1)\le be}}
    \SKIP
  \end{CASE}
\end{stuki*}

4/\elagegy{P\es\pi}\\
$f(i+1)\le ke \vagy f(i+1) \ge be \vagy ke \le f(i+1) \le be \ekv
(f(i+1)\le ke \vagy f(i+1) \ge be \vagy ke\le f(i+1)) \es
(f(i+1)\le ke \vagy f(i+1) \ge be \vagy be\ge f(i+1)) \ekv \igaz$. És
igazra minden következik.\\
4/\elagketto{P\es\pi}{Q''}\vspace{-0.8cm}
\begin{enumerate}
  \item $f(i+1)\le ke$: \\
$(Q \es b\in [m..n] \es k\in [m..n] \es i\in[m..n-1] \es f(k)=ke \es f(b)=be \es \forall j\in [m..i]:(f(j)\ge ke \es f(j)\le be) \es ke\le be \es f(i+1)\le ke)$\\
$\kovkerdes$\\
$\lf(k,ke:=i+1, f(i+1), Q'') = (Q \es i+1\in[m..n] \es b\in[m..n] \es i+1\in[m..n] \es f(i+1)=f(i+1) \es f(b)=be \es
 \underbrace{\forall j\in [m..i+1]:(f(j)\ge f(i+1) \es f(j)\le be)}_{
\forall j\in [m..i]:(f(j)\ge f(i+1) \es f(j)\le be) \es f(i+1)\ge f(i+1) \es f(i+1)\le be
}
\es f(i+1) \le be
$\\$\surd$
  \item $f(i+1)\ge be$: HF
  \item $ke\le f(i+1)\le be$:\\
$(Q \es b\in [m..n] \es k\in [m..n] \es i\in[m..n-1] \es f(k)=ke \es f(b)=be \es \forall j\in [m..i]:(f(j)\ge ke \es f(j)\le be) \es ke\le be \es ke\le f(i+1)\le be)$\\
$\kovkerdes$\\
$\lf(SKIP, Q'') = (Q \es k\in[m..n] \es b\in[m..n] \es i+1\in[m..n] \es f(k)=ke) \es f(b)=be \es$\\
$\underbrace{\forall j\in [m..i+1]:(f(j)\ge ke \es f(j)\le be)}_{
\forall j\in [m..i]:(f(j)\ge ke \es f(j)\le be) \es ke\le f(i+1) \es f(i+1)\le be
}
\es ke \le be
$\\$\surd$
\begin{stuki}
  \stm{i,b,k,be,ke:=m,m,m,f(m),f(m)}
  \begin{WHILE}{3}{\stm{i \ne n}}
    \begin{CASE}{1}{3}
      \WHEN{\stm{f(i+1)\le ke}}
      \stm{k,ke:=i+1,f(i+1)}
      \WHEN{\stm{f(i+1)\ge be}}
      \stm{b,be:=i+1,f(i+1)}
      \WHEN{\stm{ke\le f(i+1)\le be}}
      \SKIP
    \end{CASE}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

\end{enumerate}

\end{document}