\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 10. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adott az egész számokat tartalmazó x vektor. Permutáljuk a vektor 
elemeit (helyben!) úgy, hogy a vektor egy eleme a monoton rendezés szerinti helyére kerüljön,
azaz ne elõzze meg õt nála nagyobb elem és utána ne legyen nála kisebb!

Elõször egy kicsit egyszerûbb feladatot oldunk meg: a vektor egy
konkrét elemét visszük a helyére.

\emph{Megjegyzés:} Ezt a feladatot és elsõ megoldását eredetileg Hoare vezette
be, a gyorsrendezés részeként. Õ az alábbi megoldást adta (aminek helyességét
azonban nem bizonyítjuk, csak egy állapottér magyarázó táblázattal szolgálunk):

\begin{tabular}{c|l}
  A & a rendezendõ vektor \\
  i & balról lépkedõ mutató \\
  j & jobbról lépkedõ mutató (a végén mutatja a pivot elem új indexét)\\
  p & a vektor alsó indexe, egyben a pivot elem indexe \\
  r & a vektor felsõ indexe
\end{tabular}

\begin{stuki}
  \stm{x,i,j:=A[p],p+1,r}
  \begin{WHILE}{7}{\stm{i < j}}
    \begin{WHILE}{1}{\stm{A[i]\le x \es i<j}}
      \stm{i:=i+1}
    \end{WHILE}
    \begin{WHILE}{1}{\stm{A[j]\ge x \es i \le j}}
      \stm{j:=j-1}
    \end{WHILE}
    \begin{IF}{2}{\stm{i<j}}
      \stm{A[i],A[j]:=A[j],A[i]}
      \stm{i,j:=i+1,j-1}
      \ELSE
      \SKIP
    \end{IF}
  \end{WHILE}
  \stm{A[j],A[p]:=A[p],A[j]}
\end{stuki}

Mi egy másik megoldást, nevezetesen Lomuto megoldását vesszük alaposan szemügyre.  Ez
annyiban is eltér Hoare megoldásától, hogy az elsõ helyett az utolsó elemet teszi
helyre.

\emph{Specifikáció:}\\
$A = \alatt{\V}{x} \times \alatt{\Z}{i} \times \alatt{\Z}{j}$\\
$\V = \vect(\Z, \Z)$\\
$B = \alatt{\V}{x'}$\\
$Q = ( x=x' )$\\
$R = ( x\in \perm(x') \es i\in [x.lob .. x.hib] \es x_i=x'.hiv \es \forall k\in
[x.lob .. i-1]:x_k\le x_i \es \forall k\in [i+1..x.hib]:x_k>x_i )$

$x\in\perm(x')$ azt írja le, hogy az $x$ vektor elemei ugyanazok,
mint az $x'$-é, csupán a sorrendjük különbözik.

\emph{Megoldás:}\\
A megoldást könnyedén (egy megengedett szimultán értékadással elérhetnénk), ha
már teljesülne $R'$ állapot:\\
$R' = ( x\in\perm(x') \es i\in [x.lob-1 .. x.hib-1] \es x.hiv=x'.hiv \es \forall k\in
[x.lob .. i]:x_k\le x.hiv \es \forall k\in [i+1..x.hib-1]:x_k>x.hiv )$

Tûzzûk ki tehát új utófeltételnek $R'$-t és ha oda eljutunk, akkor a
szekvencia levezetési szabályát alkalmazzuk majd a meglévõ programra
és az $R$-be vezetõ $i,x_{i+1},x.hiv:=i+1,x.hiv,x_{i+1}$ értékadásra,
hogy a teljes megoldó programot kapjuk.

Most írjuk fel az új utófeltételhez elvezetõ ciklus invariánsát:\\
$P = (x\in\perm(x') \es j\in [x.lob..x.hib] \es i\in [x.lob-1 .. j-1] \es
x.hiv=x'.hiv \es \forall k\in [x.lob .. i]:x_k\le x.hiv \es
\forall k\in [i+1..j-1]:x_k>x.hiv)$

Ellenõrízzük le a ciklus feltételeit:\\
\cklegy \\
$Q' = (Q \es i=x.lob-1 \es j=x.lob)$

Látható, hogy $Q' \kov P$ és $Q \kov \lf(i,j:=x.lob-1,x.lob , Q') = Q$.

\cklketto \hspace{-2mm} $'$ \\
Ebbõl a pontból kapjuk meg a ciklusfeltételt, hiszen $P$ és $R'$ összehosonlításából
$\nem\pi$-re $x.hib=j$ adódik.  Tehát $\pi = (j \ne x.hib)$.
\begin{stuki}
  \stm{i,j:=x.lob-1,x.lob}
  \begin{WHILE}{1}{\stm{j \ne x.hib}}
    \stm{\dots}
  \end{WHILE}
  \stm{i,x_{i+1},x.hiv:=i+1,x.hiv,x_{i+1}}
\end{stuki}
\cklharom \\
Jelen esetben ez: $j\in[x.lob..x.hib-1]\es \cdots \kov t>0$. Tehát $t:=x.hib-j$
egy megfelelõ terminálófüggvény.\\
\cklnegy \\
Nézzük az alábbi struktogramot $S_0$-ként:
\begin{stuki}[8cm]
  \begin{IF}{2}{\stm{x_j\le x.hiv}}
    \stm[2]{i,j,x_{i+1},x_j:=\\i+1,j+1,x_j,x_{i+1}}
    \ELSE
    \stm{j:=j+1}
  \end{IF}
\end{stuki}
Annak bizonyítását, hogy ez az elágazás mindig növeli $j$ értékét (és
így csökkenti a termináló függvényt), az olvasóra bízom.

\cklnegy \\
Ezen állítás igazolásához az elágazás levezetési szabályának feltételeit kell ellenõríznünk:\\
4/\elagegy{P\es\pi} $\surd$

4/\elagketto{P\es\pi}{P}
\begin{enumerate}
\item $x_j\le x.hiv$:\\
$x\in\perm(x') \es j\in [x.lob..x.hib-1]\es i\in [x.lob-1 .. j-1] \es
x.hiv=x'.hiv \es \forall k\in [x.lob .. i]:x_k\le x.hiv \es
\forall k\in [i+1..j-1]:x_k>x.hiv \es x_j\le x.hiv$\\
$\kovkerdes$\\
$\lf(i,j,x_{i+1},x_j:=i+1,j+1,x_j,x_{i+1}, P)=(y\in\perm(x') \es
j+1\in [y.lob..y.hib] \es i+1\in [y.lob-1 .. j] \es
y.hiv=x'.hiv \es \forall k\in [y.lob .. i+1]:y_k\le y.hiv \es
\forall k\in [i+2..j]:y_k>y.hiv$, ahol $y.hib=x.hib \es y.lob=x.lob \es
\forall h\in[x.lob, x.hib]\setminus\{i+1,j\}: y_h=x_h \es y_{i+1}=x_j \es y_j=x_{i+1}$.
$\surd$
\item $x_j > x.hiv$:\\
$x\in\perm(x') \es j\in [x.lob..x.hib-1]\es i\in [x.lob-1 .. j-1] \es
x.hiv=x'.hiv \es \forall k\in [x.lob .. i]:x_k\le x.hiv \es
\forall k\in [i+1..j-1]:x_k>x.hiv \es x_j > x.hiv$\\
$\kovkerdes$\\
$\lf(j:=j+1, P)=(x\in\perm(x') \es j+1\in [x.lob..x.hib] \es i\in [x.lob-1 .. j] \es
x.hiv=x'.hiv \es \forall k\in [x.lob .. i]:x_k\le x.hiv \es
\forall k\in [i+1..j]:x_k>x.hiv) \surd$
\end{enumerate}

Ezzel megkaptuk a szakmában helyrevisznek becézett feladat megoldását
(ez volt a mi egyszerûsített feladatunk).
\begin{stuki*}[10cm]{helyrevisz}
  \stm{i,j:=x.lob-1,x.lob}
  \begin{WHILE}{3}{\stm{j \ne x.hib}}
    \begin{IF}{2}{\stm{x_j\le x.hiv}}
      \stm[2]{i,j,x_{i+1},x_j:=\\i+1,j+1,x_j,x_{i+1}}
      \ELSE
      \stm{j:=j+1}
    \end{IF}
  \end{WHILE}
  \stm{i,x_{i+1},x.hiv:=i+1,x.hiv,x_{i+1}}
\end{stuki*}

Ám nekünk az volt a feladatunk, hogy egy adott elemet vigyünk a helyére.  Egészítsük
ki a specifikációt ennek megfelelõen:\\
$A = \alatt{\V}{x} \times \alatt{\Z}{n} \times \alatt{\Z}{i} \times \alatt{\Z}{j}$\\
$\V = \vect(\Z, \Z)$\\
$B = \alatt{\Z}{x'} \times \alatt{\Z}{n'}$\\
$Q = ( x=x' \es n=n' \es n\in [x.lob .. x.hib])$\\
$R = ( n=n' \es x\in\perm(x') \es i\in [x.lob .. x.hib] \es x_i=x'_{n'} \es \forall k\in
[x.lob .. i-1]:x_k\le x_i \es \forall k\in [i+1..x.hib]:x_k>x_i )$

A szekvencia levezetési szabályával bizonyítható, hogy ezt a feladatot az alábbi
program oldja meg:
\begin{stuki}[10cm]
  \stm{x_n,x.hiv:=x.hiv,x_n}
  \stm{i,j:=x.lob-1,x.lob}
  \begin{WHILE}{3}{\stm{j \ne x.hib}}
    \begin{IF}{2}{\stm{x_j\le x.hiv}}
      \stm[2]{i,j,x_{i+1},x_j:=\\i+1,j+1,x_j,x_{i+1}}
      \ELSE
      \stm{j:=j+1}
    \end{IF}
  \end{WHILE}
  \stm{i,x_{i+1},x.hiv:=i+1,x.hiv,x_{i+1}}
\end{stuki}

A most megismert algoritmus legnagyobb jelentõsége, hogy a jelenleg ismert
leggyorsabb (és egyben ``leghóbortosabb'') rendezõ algoritmus szerves része.
Az érdekesség kedvéért itt közöljük egy olyan verzióját ennek a rendezõnek,
ami a modell kereteibe igazából (például a rekurzió miatt) nem illik, de
intuitíven megérthetõ.  A rendezõ mély tárgyalását az Algoritmusok és
adatszerkezetek címû tárgy keretei között hallgathatjuk meg.

\begin{stuki*}[10cm]{helyrevisz(x,i,p,r)}
  \stm{i,j:=p-1,p}
  \begin{WHILE}{3}{\stm{j \ne r}}
    \begin{IF}{2}{\stm{x_j\le x_r}}
      \stm[2]{i,j,x_{i+1},x_j:=\\i+1,j+1,x_j,x_{i+1}}
      \ELSE
      \stm{j:=j+1}
    \end{IF}
  \end{WHILE}
  \stm{i,x_{i+1},x_r:=i+1,x_r,x_{i+1}}
\end{stuki*}

\begin{stuki*}{gyorsrendezés(x,p,r)}
  \begin{WHILE}{3}{\stm{p<r}}
    \stm{\textrm{helyrevisz}(x,i,p,r)}
    \stm{\textrm{gyorsrendezés}(x,p,i-1)}
    \stm{p:=i+1}
  \end{WHILE}
\end{stuki*}
\end{document}
