\documentclass[a4paper]{article}
\usepackage{progm}
\usepackage[top=1.5cm, bottom=0.5cm]{geometry}
\analpacks
\pagestyle{empty}
\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\\2008. február 22. (péntek), 10 óra\end{center}

\emph{1. feladat \marginpar{20 pont}}\\Adott az $f:\Z\times\Z\nyil\Z$ függvény.
Határozzuk meg az $[m..n]\times[j..k]$ által kihasított értelmezési
tartományrész függvényértékei által meghatározott négyzetes mátrix
fõátlóbeli elemeinek az összegét (tehát a mátrix nyomát).  Formálisan:
az $f(m, j)+f(m+1, j+1)+\ldots+f(n, k)$ összegre vagyunk kíváncsiak.
Adjunk specifikációt, megoldóprogramot!  Bizonyítsuk be, hogy a
megoldóprogram megoldja a specifikációban kitûzõtt feladatot!

\emph{Megoldás:}\\
$A = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\Z}{j} \times
  \alatt{\Z}{k} \times \alatt{\Z}{r}$\marginpar{1 pont}\\
$B = \alatt{\Z}{m'} \times \alatt{\Z}{n'} \times \alatt{\Z}{j'} \times
  \alatt{\Z}{k'}$\marginpar{1 pont}\\
$Q = (m=m' \es n=n' \es j=j' \es k=k' \es m\le n+1 \es n-m = k-j)$ \marginpar{2 pont}\\
$R = (Q \es r=\sum\limits_{i=0}^{n-m}f(m+i, j+i))$ \marginpar{3 pont}

\noindent
$P = (Q \es z\in[-1..n-m] \es r=\sum\limits_{i=0}^z f(m+i, j+i))$ \marginpar{3 pont}

\cklegy \marginpar{1 pont}\\
$Q' := (Q \es z = -1 \es r = 0) \kov P$\\
$Q\kov \lf(z,r:=-1, 0, Q')$

\cklketto \marginpar{1 pont}\\
$\nem\pi := (z=n-m)$

\cklharom \marginpar{1 pont}\\
$t:=n-m-z$

\cklnegyot \marginpar{4 pont}\\
$(P\es\pi\es t=t_0) = $\\
$= (Q \es z\in[-1..n-m-1] \es r=\sum\limits_{i=0}^z f(m+i, j+i) \es n-m-z=t_0) \kovkerdes$\\
$\kovkerdes \lf(z,r:=z+1, r+f(m+z+1, j+z+1), Q \es z\in[-1..n-m] \es r=\sum\limits_{i=0}^z f(m+i, j+i) \es n-m-z<t_0)=$ \\
$=(Q \es z+1\in[-1..n-m] \es r+f(m+z+1, j+z+1)=\sum\limits_{i=0}^{z+1} f(m+i, j+i) \es n-m-z-1<t_0) \surd$

Tehát a megoldóprogram: \marginpar{\vspace{1cm}3 pont}
\begin{stuki}[7cm]
  \stm{z,r:=-1,0}
  \begin{WHILE}{1}{\stm{z\ne n-m}}
    \stm{z,r:=z+1, r+f(m+z+1, j+z+1)}
  \end{WHILE}
\end{stuki}

\pagebreak

\emph{2. feladat \marginpar{10 pont}}\\A gyakorlaton levezettük az alábbi
struktogramot, ami tetszõleges $n$ természetes számról (az 1 kivételével)
megállapította, hogy prím-e:

\begin{stuki}[6cm]
  \stm{k,l:=1, igaz}
  \begin{WHILE}{1}{\stm{l \es k\ne n-1}}
    \stm{k,l:=k+1,(k+1)\nmid n}
  \end{WHILE}
\end{stuki}

\vspace{-2.6cm}
\vbox{\hspace{3.2cm}$Q'$}
\vspace{1.5cm}
\vbox{\hspace{3.2cm}$R'$}
\vspace{0.5cm}

Írjuk fel az állapotteret és paraméterteret, a $Q', R'$ feltételeket,
majd specifikáljuk azt a feladatot, ami már az 1-re is helyesen
mûködik és adjuk is meg a megoldóprogramot hozzá a meglévõ struktogram
felhasználásával!  Az új program azon részének helyességét nem kell
bizonyítani, amely a $Q'$ feltételt köti össze az $R'$ feltétellel.

\emph{Megoldás: }\\
$A = \alatt{\N}{n} \times \alatt{\L}{l} \times \alatt{\N}{k}$\\
$B = \alatt{\N}{n'}$\\
$Q' = (n=n' \es n\ne 1)$\\
$R' = (Q \es l=\text{prím}(n))$\marginpar{3 pont}\\
$Q = (n=n')$\\
$R = (Q \es l=\text{prím}(n))$

\begin{stuki}[8cm]
  \begin{IF}{3}{\stm{n\ne1}}
    \stm{k,l:=1, igaz}
    \begin{WHILE}{1}{\stm{l \es k\ne n-1}}
      \stm{k,l:=k+1,(k+1)\nmid n}
    \end{WHILE}
    \ELSE
    \stm{l:=\hamis}
  \end{IF}
\end{stuki}\marginpar{\vspace{-1.5cm}2 pont}

\vspace{-3.3cm}
\vbox{\hspace{2.2cm}$Q$}
\vspace{0.3cm}
\vbox{\hspace{2.2cm}$Q'$\hspace{8.4cm}$Q'' = (n=n'=1)$}
\vspace{1.5cm}
\vbox{\hspace{1.8cm}$R'=R$\hspace{8.2cm}$R$}
\vspace{0.5cm}

Ezt a programot az elágazás levezetési szabályával kell vizsgálni:

\elagegy{Q} \marginpar{1 pont}

Ez nyilván teljesül, hiszen a következés jobb oldala a konstans igaz.

\elagketto{Q}{R}
\begin{enumerate}
\item $Q\es n\ne 1 \kovkerdes \lf(S_1, R)$, ahol $S_1$ a $Q'$-t
  $R$-rel összekötõ program.  A feladat szerint ezt nem kell
  bizonyítanunk, igaz. \marginpar{2 pont}
\item $Q''=(Q\es n=1)\kovkerdes \lf(l:=\hamis, R) =
  (Q\es\hamis=\text{prím}(n))$.  Igaz, mivel $n=1$ és az 1 nem
  prím. \marginpar{2 pont}
\end{enumerate}
\end{document}
