\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 26. feladat}
\newcommand{\csr}{\textrm{ csökkenően rendezett}}
\begin{document}
\noindent
\emph{Feladat:} Adott egy egész számokból álló vektor.  Rendezzük a vektor elemeit
(helyben) csökkenő sorrendbe! 

\emph{Specifikáció:}\\
$\V = \vect(\Z, \Z)$\\
$A = \alatt{\V}{x} \times \alatt{\Z}{k} \times \alatt{\Z}{i} \times \alatt{\Z}{j} \times \alatt{\Z}{max}$\\
$B = \alatt{\V}{x'}$\\
$Q = (x=x')$\\
$R = ( x=\perm(x') \es x \csr)$

Definiáljuk a \emph{csökkenően rendezett} fogalmát: $x$ vektor adott
$k$ indexéig csökkenően rendezett, ha $(\forall i\in
[x.lob..k-1]:x[i]\ge x[i+1]) \es (\forall i\in [k+1..x.hib]: x[k]\ge
x[i])$.  Továbbá $x$ vektor csökkenően rendezett, ha $x$ $x.hib$-ig
csökkenően rendezett.  A definíciókból következik, hogy $x$ vektor
csökkenően rendezett akkor is, ha $x$ $x.hib-1$-ig csökkenően
rendezett.  Ezért mostantól ezt értjük ezalatt.  Minden $x$ vektor
legyen definíció szerint $x.lob-1$-ig csökkenően rendezett.

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

$P = ( x=\perm(x') \es k \in [x.lob-1..x.hib-1] \es x\ k\textrm{-ig} \csr)$

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=x.lob-1)$

Látható, hogy $Q' \kov P$ (hiszen $x$ $x.lob-1$-ig mindig csökkenően rendezett) 
és $Q \kov \lf(k:=x.lob-1, Q') = Q$.

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{k:=x.lob-1}
  \begin{WHILE}{1}{\stm{\dots}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklketto \\
Ez a feltétel adja a ciklusfeltételt, hiszen $P$ és $R$ összehosonlításából
$\nem\pi$-re $k=x.hib-1$ adódik.  Tehát $\pi = (k\ne x.hib-1)$.
\begin{stuki}
  \stm{k:=x.lob-1}
  \begin{WHILE}{1}{\stm{k \ne x.hib-1}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}

\cklharom \\
Jelen esetben ez: $(Q \es k \in [x.lob-1..x.hib-2] \es \cdots) \kovkerdes t>0$, tehát
a termináló függvény: $t:=x.hib-k$.  Ez a függvény $P \es \pi$ esetén nyilván pozitív.

\cklot \\
Előrevéve az utolsó feltételt már most biztosíthatjuk, hogy a programunk lefutása
véges legyen.
\begin{stuki}
  \stm{k:=x.lob-1}
  \begin{WHILE}{1}{\stm{k \ne x.hib-1}}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
$P\es\pi\es x.hib-k=t_0 \kovkerdes\lf(k:=k+1, x.hib-k<t_0)=
x.hib-k-1<t_0 \surd$

\cklnegy \\
Könnyedén látható, hogy a jelenlegi ciklusmag ezt a feltételt nem teljesíti, hiszen \\
$\lf(S_0, P)=(x=\perm(x') \es k+1 \in [x.lob-1..x.hib-1] \es x\ \ \ k+1\textrm{-ig} \csr)$
$=: Q''$, nem következik $P \es \pi$-ből, mert $P\es\pi=(x=\perm(x') \es k \in [x.lob-1..x.hib-2] \es x\ \ \ k\textrm{-ig} \csr)$.

Ezért egy szekvencia második fele lesz az eddigi ciklusmag, míg az első fele pedig a \\
$P \es \pi \kov lf(S_{01}, Q'')$ feltételt kell teljesítse!  $S_{01}$-et egy újabb
szekvenciával könnyű felírni, aminek közbülső feltétele az, hogy $x$ ugyan még
csak $k$-ig $\csr$, de már meghatározásra került az $x[k+1..x.hib]$ részvektor
maximális eleme (pontosabban annak indexe).  Formálisan:\\
$Q''' = (x=\perm(x') \es k+1 \in [x.lob-1..x.hib-1] \es x\ \ \ k\textrm{-ig} \csr \es
i\in[k+1..x.hib] \es \forall j\in[k+1..x.hib]:x[j]\le x[i])$\\
Most vizsgáljuk meg a $\lf(x[k+1],x[i]:=x[i],x[k+1], Q'')$ feltételt:\\
$x^{k+1\knyil i}=\perm(x') \es k+1 \in [x.lob-1..x.hib-1] \es x^{k+1\knyil i}\ \ \ k+1\textrm{-ig} \csr$\\
Ennek a feltételnek az első két konjunkciós része nyilván következik $Q'''$-ből,
csupán az a kérdés, hogy a harmadik résszel mi a helyzet?  Természetesen $x^{k+1\knyil i}\ \ \ k+1\textrm{-ig} \csr$
akkor és csak akkor, ha $x^{k+1\knyil i}\ \ \ k\textrm{-ig} \csr$ és $x^{k+1\knyil i}[k+1]$ elválasztó
elem (abban az értelemben, hogy $k$ indexig minden elem nagyobb vagy egyenlő, $k+1$ indextől minden elem kisebb
vagy egyenlő vele a vektorban).\\
Ezt a meggondolást felhasználva $Q'''$-ből láthatóan következik a harmadik rész,
ugyanis $Q'''$ fennállása esetén $i\ge k+1$, azaz az, hogy $x^{k+1\knyil i}\ \ \ k\textrm{-ig} \csr$
pontosan ugyanazt jelenti, mint az, hogy $x\ \ \ k\textrm{-ig} \csr$, ami már $Q'''$ része.\\
$x^{k+1\knyil i}[k+1]$ pedig elválasztó elem $Q'''$ szerint, hiszen ez pont az $x[i]$ elem
a házi jelölésünk értelmében (ld. 10. feladat megoldása).  De az $x[i]$ elem maximális a
$k+1$ indextől kezdődő részen $Q'''$ szerint, továbbá minden elem $k+1$ után (mivel
$x$ $k$-ig $\csr$) kisebb, mint a $k$ előtti elemek, így $x[i]$ is, tehát ő elválasztó
elem.\\
Összességében $Q'''\kov\lf(x[k+1],x[i]:=x[i],x[k+1], Q'')$.

Már csak azt a $S_{010}$ programot kell megtalálnunk, amivel $P\es\pi\kov Q'''$.  Ez a maximumkereséshez
nagyon hasonló (de vektorrészleten működő) program, aminek levezetése a maximumkeresés
programozási tételének levezetése ismeretében triviális, ezért itt csak a stuktogramot közöljük
a kész program részeként:

\begin{stuki}
  \stm{k:=x.lob-1}
  \begin{WHILE}{7}{\stm{k \ne x.hib-1}}
    \stm{i,j,max:=k+1,k+1,f(k+1)}
    \begin{WHILE}{3}{\stm{j\ne x.hib}}
      \begin{IF}{1}{\stm{f(j+1)>max}}
        \stm{i,max:=j+1,f(j+1)}
        \ELSE
        \SKIP
      \end{IF}
      \stm{j:=j+1}
    \end{WHILE}
    \stm{x[k+1],x[i]:=x[i],x[k+1]}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

\begin{textblock}{1}(2.4,-3.35)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{4.7cm}\\$R$
\end{textblock}
\begin{textblock}{1}(10.4,-2.64)
$P \es \pi$
\vspace{2.7cm}\\$Q'''$
\vspace{0.2cm}\\$Q''$
\end{textblock}
\end{document}