\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 ix_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