\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. zárthelyi dolgozat, 2006. 03. 09.}
\begin{document}
\noindent
,,Before software can be reusable it first has to be usable.''\\
--- Ralph Johnson

\begin{center}Bevezetés a programozáshoz 2., 1. zárthelyi dolgozat (megoldás)\\2006. március 9. (csütörtök), 8 óra\end{center}

Specifikáld az alábbi feldatokat, majd add meg a megoldó programokat
és helyességük bizonyítását!

\emph{1. Feladat}\\Határozzuk meg az $n!=1\cdot2\cdots n$ értékét! (13 pont)

\emph{Specifikáció:} (3 pont)\\
$A = \alatt{\N_0}{n} \times \alatt{\N}{r}$\\
$B = \alatt{\Z}{n'}$\\
$Q = ( n=n' )$\\
$R = ( Q \es r=n!)$

\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{\N_0}{n} \times \alatt{\N}{r} \times \alatt{\N_0}{k}$\\
$P  = (Q \es k\in [0..n] \es r=k!)$ (2 pont)

Ellenõrízzük le a ciklus feltételeit:\\
\cklegy (1 pont)\\
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=0 \es r=1 )$

Látható, hogy $Q' \kov P$ és $Q \kov \lf(k,r:=0,1 , Q') = ( Q \es 0=0 \es 1=1 ) = Q$.

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

\cklnegyot (3 pont)\\

A ciklusmagban $k$ értékét biztos növeljük, viszont az invariánst is
meg kell tartanunk, ezt teszi egyszerre a $k,r:=k+1,r(k+1)$ szimultán
értékadás, lássuk mi ennek a leggyengébb elõfeltétele a $P \es
t=t_0$-ra vonatkozóan: $\lf(k,r:=k+1,r(k+1), P \es n-k=t_0) = ( Q \es
k+1\in [0..n] \es r(k+1)=(k+1)! \es n-k-1 = t_0 )$.  Ez a feltétel
azonban következik $P \es \pi \es t=t_0$-ból.

\begin{stuki}[6cm]
  \stm{k,r:=0,1}
  \begin{WHILE}{1}{\stm{k \ne n}}
    \stm{k,r:=k+1,r(k+1)}
  \end{WHILE}
\end{stuki}
\vspace{-2cm}(2 pont)\vspace{2cm}\\
\emph{2. Feladat}\\Határozzuk meg az ,,n alatt a k'' értékét, kétféleképpen:
\begin{itemize}
\item Az elõzõ feladat programjának segítségével, matematikai segítség: ${n\choose k}=\frac{n!}{k!(n-k)!}$ (7 pont)

\emph{Specifikáció:} (1 pont)\\
$A = \alatt{\N}{n} \times \alatt{\N}{k} \times \alatt{\N}{r}$\\
$B = \alatt{\N}{n'} \times \alatt{\N}{k'}$\\
$Q = ( n=n' \es k=k' \es k\le n )$\\
$R = ( Q \es r=\frac{n!}{k!(n-k)!})$

\emph{Megoldás:} (6 pont)\\
Kiterjesztjük az állapotteret, bevezetünk egy --- az $n-k$ értékét
tartalmazó --- $nk$ nevû változót, valamint $nf, kf, nkf$ változókat,
amik a faktoriálisokat fogják tartalmazni.  Felírünk pár köztes állapotot is:\\
$A' = \alatt{\N}{n} \times \alatt{\N}{k} \times \alatt{\N}{r} \times \alatt{\N}{nk} \times \alatt{\N}{nf} \times \alatt{\N}{kf} \times \alatt{\N}{nkf}$\\
$Q' = ( Q \es nk = n - k )$\\
$Q'' = ( Q' \es nf = n! )$\\
$Q''' = ( Q'' \es kf = k! )$\\
$Q'''' = ( Q''' \es nkf = (n-k)! )$

Ekkor: $Q \kov \lf(nk:=n-k, Q')$, valamint $Q'$-bõl $Q''$, $Q''$-bõl
$Q'''$ és $Q'''$-bõl $Q''''$ az elõzõ feladat megoldásaként kapott
programmal (persze más változókat használva) elérhetõ, azokat a
részeket újra nem bizonyítjuk.  Továbbá: $Q'''' \kov
\lf(r:=\frac{nf}{kf*nkf})=(Q \es \frac{nf}{kf*nkf} =
\frac{n!}{k!(n-k)!})$.  Így a szekvencia levezetési szabálya miatt
$Q\kov lf(S,R)$, ami pont azt jelenti, hogy a program megoldja a
feladatot.

\begin{stuki}[6cm]
  \stm{nk:=n-k}
  \stm{i,nf:=0,1}
  \begin{WHILE}{1}{\stm{i \ne n}}
    \stm{i,nf:=i+1,nf(i+1)}
  \end{WHILE}
  \stm{i,kf:=0,1}
  \begin{WHILE}{1}{\stm{i \ne k}}
    \stm{i,kf:=i+1,kf(i+1)}
  \end{WHILE}
  \stm{i,nkf:=0,1}
  \begin{WHILE}{1}{\stm{i \ne nk}}
    \stm{i,nkf:=i+1,nkf(i+1)}
  \end{WHILE}
  \stm{r:=\frac{nf}{kf*nkf}}
\end{stuki}
\begin{textblock}{1}(9.2,-3.97)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{1.6cm}\\$Q''$
\vspace{1.4cm}\\$Q'''$
\vspace{1.5cm}\\$Q''''$
\vspace{0.2cm}\\$R$
\end{textblock}

Mejegyzés: a struktogrammban szereplõ $i$ az állapottér egy új, $N_0$
értékû komponense.

\item Más, hatékonyabb módon, segítség: ${n\choose k}=\frac{n\cdot(n-1)\cdots(n-k+1)}{k\cdot(k-1)\cdots1}$ (15 pont)

\emph{Specifikáció:} (5 pont)\\
$A = \alatt{\N}{n} \times \alatt{\N}{k} \times \alatt{\Q}{r}$\\
$B = \alatt{\N}{n'} \times \alatt{\N}{k'}$\\
$Q = ( n=n' \es k=k' \es k\le n )$\\
$R = \left( Q \es r=\prod\limits_{j=1}^{k}\frac{n-k+j}{j}(=\frac{n!}{k!(n-k)!})\right)$

\emph{Megoldás:}\\
$A' = \alatt{\N}{n} \times \alatt{\N}{k} \times \alatt{\N}{r} \times \alatt{\N_0}{i}$\\
$P = \left( Q \es i\in[0..k] \es r=\prod\limits_{j=1}^{i}\frac{n-k+j}{j})\right)$ (3 pont) \\
\cklegy (1 pont): $Q' = ( Q \es i = 0 \es r = 1 )$\\
\cklketto (1 pont): $\pi = (i\ne k)$\\
\cklharom (1 pont): $t = n-i$\\
\cklnegyot (3 pont): $S_0 : ( i,r:=i+1,r\frac{n-k+i+1}{i+1} ) $

\begin{stuki}[6cm]
  \stm{i,r:=0,1}
  \begin{WHILE}{1}{\stm{i \ne k}}
    \stm{i,r:=i+1,r\frac{n-k+i+1}{i+1}}
  \end{WHILE}
\end{stuki}
\vspace{-2cm}(1 pont)\vspace{2cm}\\
\end{itemize}

\emph{3. Feladat}\\Adott a $t$ négyzetes mátrix.  Tükrözzük (transzponáljuk) a mellékátlójára helyben (azaz az eredmény
$t$-ben keletkezzen)! (25 pont)

Szóhasználat: azt fogjuk mondani, hogy $t$ az elsõ $n$ sorában transzponáltja $t'$-nek, ha
$\forall i\in[0,n-1]:(\forall j\in[0,t.dom-i-1]:({t_{t.lob+i}}_{t.lob+j}={t'_{t.hib-j}}_{t.hib-i} \es {t_{t.hib-j}}_{t.hib-i}={t'_{t.lob+i}}_{t.lob+j}))$.  Másrészt $t$ $n+1.$ sora az $i+1.$ elemig transzponálva van, ha $\forall j\in[0,i]:({t_{t.lob+n}}_{t.lob+j}={t'_{t.hib-j}}_{t.hib-n} \es {t_{t.hib-j}}+{t.hib-n} = {t'_{t.lob+n}}_{t.lob+j})$

\emph{Specifikáció:} (6 pont)\\
$\M = \vect(\Z, \vect(\Z,\Z))$, invariánsa: $I(x) = (\forall i\in[x.lob,x.hib]: x_i.lob = x.lob \es x_i.hib = x.hib)$\\
$A = \alatt{\M}{t}$\\
$B = \alatt{\M}{t'}$\\
$Q = (t=t')$\\
$R = (t$ az elsõ $t.dom$ sorában transzponáltja $t'$-nek$)$

\emph{Megoldás:}\\
$A' = \alatt{\M}{t} \times \alatt{\N_0}{k} \times \alatt{\N_0}{l}$\\
$P  = (k\in [0,t.dom] \es t$ az elsõ $k$ sorában transzponáltja $t'$-nek$)$ (3 pont)\\
\cklegy (1 pont): $Q' = ( Q \es k = 0 )$\\
\cklketto (1 pont): $pi = ( k \ne t.dom )$\\
\cklharom (1 pont): $t^* = t.dom - k)$\\
\cklnegyot: egy szekvenciával, aminek elsõ fele egy újabb ciklus:\\
$R_b = Q'' = (k\in [0,t.dom-1] \es t$ az elsõ $k+1$ sorában transzponáltja $t'$-nek $\es t^*=t^*_0)$ (1 pont)\\
vegyük észre: $R_b = (k\in [0,t.dom-1] \es t$ az elsõ $k$ sorában transzponáltja $t'$-nek $\es t^*=t^*_0 \es t$ $k+1.$ sora az $t.dom-k$ elemig transzponálva van.$)$ \\
$R_b\kov\lf(k:=k+1, P \es t^*<t^*_0)$ (1 pont)\\
$Q_b = (P \es \pi \es t^* = t^*_0) = (k\in [0,t.dom-1] \es t$ az elsõ $k$ sorában transzponáltja $t'$-nek $\es t^*=t^*_0)$\\
$P_b = (k\in [0,t.dom-1] \es l\in[0, t.dom-k] \es t$ az elsõ $k$ sorában transzponáltja $t'$-nek $\es t^*=t^*_0 \es t$ $k+1.$ sora az $l$ elemig transzponálva van.$)$ (3 pont)\\
$Q'_b = (k\in [0,t.dom-1] \es l=0 \es t$ az elsõ $k$ sorában transzponáltja $t'$-nek$)$\\
$\pi_b = (l \ne t.dom-k)$ (1 pont)\\
$t^*_b = (t.dom-k - l)$ (1 pont)\\
$Q''_b = (k\in [0,t.dom-1] \es l\in[0, t.dom-k-1] \es t$ az elsõ $k$ sorában transzponáltja $t'$-nek $\es t^*=t^*_0 \es t$ $k+1.$ sora az $l+1$ elemig transzponálva van. $\es t^*_b = {t^*_b}_0)$ (3 pont)\\
\begin{stuki}[13cm]
  \stm{k:=0}
  \begin{WHILE}{5}{\stm{k \ne t.dom}}
    \stm{l:=0}
    \begin{WHILE}{2}{\stm{l \ne t.dom-k}}
      \stm{{t_{t.lob+k}}_{t.lob+l},{t_{t.hib-l}}_{t.hib-k}:={t'_{t.hib-l}}_{t.hib-k},{t'_{t.lob+k}}_{t.lob+l}}
      \stm{l:=l+1}
    \end{WHILE}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
\begin{textblock}{3}(11.5,-2.59)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{0.2cm}\\$Q_b$
\vspace{0.2cm}\\$Q'_b$
\vspace{0.2cm}\\$P_b \es \pi_b \es t^*_b = {t^*_b}_0$
\vspace{0.2cm}\\$Q''_b$
\vspace{0.2cm}\\$R_b$
\vspace{0.2cm}\\$R$
\end{textblock}
\vspace{-3cm}(3 pont)


\end{document}
