\documentclass[a4paper]{article}
\usepackage{progm}
\usepackage{graphicx}
\usepackage{cancel}
\usepackage[top=1.0cm, bottom=1.0cm]{geometry}
\setlength{\parindent}{0pt}
\analpacks
\pagestyle{empty}
\begin{document}
\begin{center}Bevezetés a programozáshoz 2., 2. zárthelyi dolgozat\\2008. március 7. (péntek), 10 óra\end{center}

\emph{1. feladat}\\
Adott az $x$ vektor és a vele azonos értelmezési tartományú (lob-ot és
hib-et, így dom-ot tekintve is megegyezõ) $y$ vektor.  $x$ elemei
természetes számok és nincs köztük két egyforma.
\begin{itemize}
\item Fogalmazzuk meg szövegesen, hogy milyen feladatot old meg az
  alább specifikált feladat!\marginpar{3 pont}
\item Írjunk megoldóprogramot és bizonyítsuk be a helyességét
  levezetéssel! (Használhatjuk a szereplõ hely nevû függvényt a
  programban is bárhol.) \marginpar{8 pont}
\item Specifikáljunk egy feladatot és adjunk megoldóprogramot
  levezetéssel a hely függvény kiszámítására egy adott $x$ vektor egy
  adott $i$ elemére. \marginpar{7 pont}
\end{itemize}

\noindent
$\V=\vect(\Z, \N)$\\
$A=\alatt{\V}{x} \times \alatt{\V}{y}$\\
$B=\alatt{\V}{x'}$\\
$Q: (x=x' \es y.\lob=x.\lob \es y.\hib=x.\hib \es \forall i,j\in[x.\lob,x.\hib]: i\ne j\nyil x_i\ne x_j)$\\
$R: ( Q \es \forall i\in[x.\lob,x.\hib]: y_{\text{hely}(x,i)} = x_i)$, ahol $\text{hely}(x,i)=x.\lob+\sum\limits_{j=x.\lob}^{x.\hib}\chi(x_j<x_i)$

\emph{Megoldás:}\\
A feladat az\marginpar{3 pont}, hogy rendezzük az $x$ vektort növekvõ
sorrendbe, az eredmény $y$-ban keletkezzen!

$P: ( Q \es k\in[x.\lob-1,x.\hib] \es \forall i\in[x.\lob, k]: y_{\text{hely}(x,i)} = x_i )$\marginpar{1 pont}

\cklegy

$Q': (Q \es k=x.\lob-1)$ \marginpar{1 pont}

\cklketto

$\nem \pi = ( k = x.\hib )$\marginpar{1 pont}

\cklharom

$t:=x.\hib-k$\marginpar{1 pont}

\cklnegyot

\begin{stuki}[6cm]
  \stm{k:=x.\lob-1}
  \begin{WHILE}{1}{\stm{k\ne x.\hib}}
    \stm{y_{\text{hely}(x,k+1)},k := x_{k+1},k+1}
  \end{WHILE}
\end{stuki}

\vspace{-2.6cm}
\vbox{\hspace{3.9cm}$Q$}
\vspace{0.2cm}
\vbox{\hspace{3.9cm}$Q'$}
\vspace{0.3cm}
\vbox{\hspace{10.5cm}$P\es\pi$}\marginpar{2 pont}
\vspace{0.2cm}
\vbox{\hspace{3.9cm}$R$}
\vspace{0.5cm}

\[
\begin{array}{ccc}
  P\es\pi\es t=t_0 & \kovkerdes & \lf(y_{\text{hely}(x,k+1)}, k := x_{k+1}, k+1, P \es t<t_0) \\
  \Arrowvert & & \Arrowvert \\
  \left. \begin{array}{c}
      Q \es k\in[x.\lob-1,x.\hib-1] \es \\
      \forall i\in[x.\lob, k]: y_{\text{hely}(x,i)} = x_i \es \\
      x.\hib-k = t_0
    \end{array}\right\} & \kovkerdes & \left\{
    \begin{array}{c}
      Q \es k+1\in[x.\lob-1,x.\hib] \es \\
      \forall i\in[x.\lob, k\cancel{+1}]: y_{\text{hely}(x,i)} = x_i \es \\
      \cancelto{x_{k+1}}{y_{\text{hely}(x,k+1)}} = x_{k+1} \es \\
      x.\hib-k-1 < t_0
    \end{array}\right.
\end{array}
\]
\marginpar{\vspace{-2cm}2 pont}

A hely függvény:\\
$A = \alatt{\V}{x}\times\alatt{\Z}{i} \times \alatt{\Z}{r}$\\
$B = \alatt{\V}{x'}\times\alatt{\Z}{i'}$ \marginpar{1 pont} \\
$Q: (x=x' \es i=i' \es i\in [x.\lob,x.\hib])$ \\
$R: (Q \es r = \text{hely}(x,i) = x.\lob + \sum\limits_{j=x.\lob}^{x.\hib}\chi (x_j<x_i))$

$P: (Q \es j\in[x.\lob-1, x.\hib] \es r = x.\lob + \sum\limits_{j=x.\lob}^{j}\chi (x_j<x_i))$ \marginpar{1 pont}\\
\cklegy \\
$Q': (Q \es j=x.\lob-1 \es r=x.\lob)$ \marginpar{1 pont}

\cklketto \\
$\nem\pi = (j\ne x.\hib)$ \marginpar{1 pont}

\cklharom \\
$t:=x.\hib-j$ \marginpar{1 pont}

\cklnegyot \\
Az elágazás levezetési szabályával levezethetõ. \marginpar{1 pont}

\begin{stuki}[6cm]
  \stm{j,r:=x.\lob-1, x.\lob}
  \begin{WHILE}{2}{\stm{j\ne x.\hib}}
    \begin{IF}{1}{\stm{x_{j+1}<x_i}}
      \stm{r,j:=r+1,j+1}
      \ELSE
      \stm{j:=j+1}
    \end{IF}
  \end{WHILE}
\end{stuki}
\marginpar{\vspace{-2cm}1 pont}

\emph{2. feladat\marginpar{12 pont}}\\
Adott az $x$ vektor, amely természetes számokat és nullákat tartalmaz,
azonban biztosan természetes számmal kezdõdik.  Írjuk minden 0 elem
helyére az elõtte szereplõ természetes számot!

\noindent
Pl. a $<2,0,0,3,4,0,5,4>$ vektort helyben a $<2,2,2,3,4,4,5,4>$
vektorrá alakítsuk!

\noindent
Specifikáljuk a feladatot és adjunk megoldóprogramot a levezetés módszerével!

\noindent
Segítség: $\forall i\in[x.\lob,x.\hib]: f(x,i):=\begin{cases}
  x_i & \text{, ha } x_i\ne 0 \\
  f(x, i-1) & \text{, ha } x_i = 0
\end{cases}$

\emph{Megoldás:}\\
$\V = \vect(\Z, \N_0), I_\V(v) = (v.\text{lov} \ne 0)$\\
$A = \alatt{\V}{x}$\\
$B = \alatt{\V}{x'}$\marginpar{4 pont} \\
$Q: (x=x')$\\
$R: (\forall i\in[x.\lob,x.\hib]: x_i=f(x', i))$

$P: (j\in[x.\lob,x.\hib] \es \forall i\in[x.\lob,j]: x_i = f(x',i) \es \forall i\in[j+1, x.\hib]: x_i = x'_i)$ \marginpar{2 pont}\\
Az invariáns azt írja le, hogy egy bizonyos pontig ($j$) az $f$ szerint
vannak már kiszámolva a vektorban az elemek, utána viszont még
változatlan a vektor.

\cklegy \vspace{5mm} Felhasználva a vektor invariánsát is:\\
$Q': ( Q \es j=x.\lob) \kov P$ \marginpar{1 pont}

\cklketto \\ $\nem\pi = (j\ne x.\hib)$\marginpar{1 pont}

\cklharom \\ $t:=x.\hib-j$\marginpar{1 pont}

\cklnegy

\marginpar{2 pont}
Elágazás aszerint, hogy $x_{j+1}$ nulla-e.  A levezetési szabály elsõ pontja triviálisan teljesül.\\
A második pont elsõ fele:
\[
\begin{array}{ccc}
  P\es\pi\es t=t_0 \es x_{j+1} = 0  & \kovkerdes & \lf(j,x_{j+1}:=j+1, x_j, P \es t<t_0) \\
  \Arrowvert & & \Arrowvert \\
  \left. \begin{array}{c}
      j\in[x.\lob,x.\hib-1] \es \\
      \forall i\in[x.\lob,j]: x_i = f(x',i) \es \\
      \forall i\in[j+1, x.\hib]: x_i = x'_i) \es \\
      x_{j+1} = 0 \es x.\hib-j = t_0
    \end{array}\right\} & \kovkerdes & \left\{
    \begin{array}{c}
      j+1\in[x.\lob,x.\hib] \es  \\
      \forall i\in[x.\lob,j\cancel{+1}]: x_i = f(x',i) \es \\
      \cancelto{x_j}{x_{j+1}} = \underbrace{f(x', j+1)}_{f(x',j)=x_j} \es \\
      \forall i\in[j+2, x.\hib]: x_i = x'_i \es \\
      x.\hib-j-1 < t_0
    \end{array}\right.
\end{array}
\]

A másik ág a $j:=j+1$ értékadással bizonyítható.

\marginpar{\vspace{1.5cm}1 pont}
\begin{stuki}[7cm]
  \stm{j:=x.\lob}
  \begin{WHILE}{2}{\stm{j\ne x.\hib}}
    \begin{IF}{1}{\stm{x_{j+1}= 0}}
      \stm{j,x_{j+1}:=j+1, x_j}
      \ELSE
      \stm{j:=j+1}
    \end{IF}
  \end{WHILE}
\end{stuki}

\emph{Megjegyzés:}

Vegyük észre, hogy ezt a második programot felhasználva az elsõ
program eredménye korrigálható abban az esetben, ha a rendezendõ
vektor tartalmazott azonos elemeket.  Ugyanis ekkor az
eredményvektorban az azonos értékeket tartalmazandó rész elsõ eleme
lesz az érték, a többihez az elsõ program nem nyúl.  Így, ha azok mindegyike
kezdetben nulla (vagy valami más kinevezett, de egyébként nem szereplõ
érték), akkor a második feladat megoldását lefuttatva az $y$
(fél)eredmény vektoron immáron helyesen rendezett vektort kapunk.
\end{document}
