\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 9. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adott egy egész számokból álló vektor és két egész szám.
Állapítsuk meg, hogy a két szám elõfordul-e a vektorban, és ha igen,
akkor melyik elõbb!

\emph{Specifikáció:}\\
$\V = \vect(\Z, \Z)$\\
$A = \alatt{\V}{v} \times \alatt{\Z}{z_1} \times \alatt{\Z}{z_2} \times \alatt{\L}{l_1} \times \alatt{\L}{l_2} \times \alatt{\{1,2\}}{r} \times \alatt{\Z}{rsz} \times \alatt{\Z}{k}$\\
$B = \alatt{\V}{v'} \times \alatt{\Z}{z_1'} \times \alatt{\Z}{z_2'}$\\
$Q = ( v=v' \es z_1=z_1' \es z_2=z_2' \es z_2 \ne z_1 )$\\
$R = ( Q \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..v.hib]: z_i=v[j]) \es (l_1 \es l_2) \nyil (r=1 \knyil g(z_1) < g(z_2)) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r)$, ahol \\
$\mathcal{D}_g = \{x\in \Z|\exists i\in [v.lob .. v.hib]: v[i]=x\}, \forall x\in \mathcal{D}_g:g(x):=i$, ha
$i\in [v.lob .. v.hib] \es v[i]=x \es \forall j\in [v.lob .. i-1]: v[j]\ne x$\\
Informálisan: g(x) x elsõ elõfordulásának indexét adja meg a vektorban.  A specifikáció tehát azt írja
le, hogy a két logikai változó külön-külön mutatja a program lefutása végén, hogy elõfordulnak-e az adott
egész számok. Ha mindkettõ elõfordul, akkor a korábban elõforduló számot tartalmazza $rsz$ és a hozzá tartozó
``indexet'' $r$.  Amennyiben csak az egyik szám fordul elõ, akkor az $rsz$ ezt a számot, míg az $r$ az
``indexét'' tartalmazza.

\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  = (Q \es k\in[v.lob-1..v.hib] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k]: z_i=v[j]) \es (l_1 \es l_2) \nyil (r=1 \knyil g(z_1) < g(z_2)) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r)$

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=v.lob-1 \es l_1=\hamis \es l_2=\hamis)$

Látható, hogy $Q' \kov P$ és $Q \kov \lf(k,l_1,l_2:=v.lob-1,\hamis,\hamis , Q') = Q$.

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{k,l_1,l_2:=v.lob-1,\hamis,\hamis}
  \begin{WHILE}{1}{\stm{\dots}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklketto \\
Ez a feltétel kezünkbe adja a ciklusfeltételt, hiszen $P$ és $R$ összehosonlításából
$\nem\pi$-re $k=v.hib$ adódik.  Ugyanakkor az állítás még akkor is igaz, ha hozzávesszük
$\vagy l_1 \es l_2$-t.  Tehát $\pi = (k \ne v.hib \es \nem (l_1 \es l_2))$.
\begin{stuki}
  \stm{k,l_1,l_2:=v.lob-1,\hamis,\hamis}
  \begin{WHILE}{1}{\stm{k \ne v.hib \es \nem (l_1 \es l_2)}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}
\cklharom \\
Jelen esetben ez: $Q \es k\in[v.lob-1..v.hib-1]\es \cdots \kov t>0$. Tehát $t:=v.hib-k$
egy megfelelõ terminálófüggvény.\\
\cklot \\
Elõrevéve az utolsó feltételt már most biztosíthatjuk, hogy a programunk lefutása
véges legyen.  Mivel $t=v.hib-k$ és $v.hib$ az invariáns szerint nem változhat, a megoldás
csak $k$ növelése lehet.
\begin{stuki}
  \stm{k,l_1,l_2:=v.lob-1,\hamis,\hamis}
  \begin{WHILE}{1}{\stm{k \ne v.hib \es \nem (l_1 \es l_2)}}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
$P\es\pi\es t=t_0 \kov t=t_0 \ekv v.hib-k=t_0 \kovkerdes\lf(S_0, v.hib-k<t_0)=v.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)=
(Q \es k+1\in[v.lob-1..v.hib] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k+1]: z_i=v[j]) \es (l_1 \es l_2) \nyil (r=1 \knyil g(z_1) < g(z_2)) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r) =: Q''$, nem következik $P \es \pi$-bõl (például abban az esetben, ha $l_1$ hamis, de
$v[k+1]=z_1$).

Ezért egy szekvencia második fele lesz az eddigi ciklusmag és $Q''$-t pedig a következõ elágazással
érjük el a szekvencia elsõ részében:

\begin{stuki}[17cm]
    \begin{CASE}[2]{2}{7}
      \WHEN[1]{\stm[2]{z_1\ne v[k+1] \es \\ z_2 \ne v[k+1]}}
      \stm[2]{SKIP}
      \WHEN[1]{\stm[2]{\nem l_1 \es \nem l_2 \\ \es v[k+1]=z_1}}
      \stm[2]{l_1,r,rsz:=\\\igaz,1,z_1}
      \WHEN[1]{\stm[2]{\nem l_1 \es \nem l_2 \\ \es v[k+1]=z_2}}
      \stm[2]{l_2,r,rsz:=\\\igaz,2,z_2}
      \WHEN[1]{\stm[2]{\nem l_1 \es  l_2 \es \\ v[k+1]=z_1}}
      \stm[2]{l_1:=\\\igaz}
      \WHEN[1]{\stm[2]{\nem l_1 \es l_2 \es \\ v[k+1] \ne z_1}}
      \stm[2]{SKIP}
      \WHEN[1]{\stm[2]{\nem l_2 \es l_1 \es \\ v[k+1]=z_2}}
      \stm[2]{l_2:=\\\igaz}
      \WHEN[1]{\stm[2]{\nem l_2 \es l_1 \es \\ v[k+1] \ne z_2}}
      \stm[2]{SKIP}
    \end{CASE}
\end{stuki}
$P\es \pi \kov lf(IF, Q'')$\\
Ezen állítás igazolásához az elágazás levezetési szabályának feltételeit kell ellenõríznunk:\\
4/\elagegy{P\es\pi}\\
A feltételek közös diszjunkciójának átalakításaival megkaphatjuk, hogy az említett diszjunkció
csak abban az esetben lehet hamis, ha $l_1 \es l_2$, ezt azonban $P \es \pi$ kizárja.\\
4/\elagketto{P\es\pi}{Q''}
\begin{enumerate}
\item $z_1\ne v[k+1] \es  z_2 \ne v[k+1] \vagy  l_1 \es l_2$ \\
$Q \es k\in[v.lob-1..v.hib-1] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k]: z_i=v[j]) \es \nem (l_1 \es l_2) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r) \es z_1\ne v[k+1] \es  z_2 \ne v[k+1]$\\
$\kovkerdes$
$lf(SKIP, Q'') = (Q \es k+1\in[v.lob-1..v.hib] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k+1]: z_i=v[j]) \es (l_1 \es l_2) \nyil (r=1 \knyil g(z_1) < g(z_2)) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r)\surd$
\item $\nem l_1 \es \nem l_2 \es v[k+1]=z_1$ \\
$Q \es k\in[v.lob-1..v.hib-1] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k]: z_i=v[j]) \es \nem (l_1 \es l_2) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r) \es v[k+1]=z_1 \es \nem l_1 \es \nem l_2$\\
$\kovkerdes$
$lf(l_1,r,rsz:=\igaz,1,z_1, Q'') = (Q \es k+1\in[v.lob-1..v.hib] \es \igaz=(\exists j \in [v.lob..k+1]: z_1=v[j]) \es l_2=(\exists j \in [v.lob..k+1]: z_2=v[j]) \es (\igaz \es l_2) \nyil (1=1 \knyil g(z_1) < g(z_2)) \es (\igaz \es \nem l_2) \nyil 1=1 \es (l_2 \es \nem \igaz) \nyil 1=2 \es (\igaz \vagy l_2) \nyil z_1=z_1)])\surd$ ($g(z_1)<g(z_2)$ állításrész $v[k+1]=z_1 \es \nem l_1 \es \nem l_2$ miatt igaz.)
\item $\nem l_1 \es \nem l_2 \es v[k+1]=z_2$\\
  hasonlóan
\item $\nem l_1 \es  l_2 \es v[k+1]=z_1$ \\
$Q \es k\in[v.lob-1..v.hib-1] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k]: z_i=v[j]) \es \nem (l_1 \es l_2) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r) \es z_1=v[k+1] \es  l_2 \es \nem l_1$\\
$\kovkerdes$
$lf(l_1:=igaz, Q'') = (Q \es k+1\in[v.lob-1..v.hib] \es igaz=(\exists j \in [v.lob..k+1]: z_1=v[j]) \es l_2=(\exists j \in [v.lob..k+1]: z_2=v[j]) \es (\igaz \es l_2) \nyil (r=1 \knyil g(z_1) < g(z_2)) \es (\igaz \es \nem l_2) \nyil r=1 \es (l_2 \es \nem \igaz) \nyil r=2 \es (\igaz \vagy l_2) \nyil rsz=z_r)\surd$
\item $\nem l_1 \es l_2 \es v[k+1] \ne z_1$ \\
$Q \es k\in[v.lob-1..v.hib-1] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k]: z_i=v[j]) \es \nem (l_1 \es l_2) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r) \es z_1\ne v[k+1] \es  l_2 \es \nem l_1$\\
$\kovkerdes$
$lf(SKIP, Q'') = (Q \es k+1\in[v.lob-1..v.hib] \es \forall i\in [1..2]: l_i=(\exists j \in [v.lob..k+1]: z_i=v[j]) \es (l_1 \es l_2) \nyil (r=1 \knyil g(z_1) < g(z_2)) \es (l_1 \es \nem l_2) \nyil r=1 \es (l_2 \es \nem l_1) \nyil r=2 \es (l_1 \vagy l_2) \nyil rsz=z_r)\surd$
\item $\nem l_2 \es l_1 \es v[k+1]=z_2$ \\
  hasonlóan, mint 4.
\item $\nem l_2 \es l_1 \es v[k+1] \ne z_2$ \\
  hasonlóan, mint 5.
\end{enumerate}

\begin{stuki}[17cm]
  \stm{k,l_1,l_2:=v.lob-1,\hamis,\hamis}
  \begin{WHILE}{5}{\stm{k \ne v.hib \es \nem (l_1 \es l_2)}}
    \begin{CASE}[2]{2}{7}
      \WHEN[1]{\stm[2]{z_1\ne v[k+1] \es \\ z_2 \ne v[k+1]}}
      \stm[2]{SKIP}
      \WHEN[1]{\stm[2]{\nem l_1 \es \nem l_2 \\ \es v[k+1]=z_1}}
      \stm[2]{l_1,r,rsz:=\\\igaz,1,z_1}
      \WHEN[1]{\stm[2]{\nem l_1 \es \nem l_2 \\ \es v[k+1]=z_2}}
      \stm[2]{l_2,r,rsz:=\\\igaz,2,z_2}
      \WHEN[1]{\stm[2]{\nem l_1 \es  l_2 \es \\ v[k+1]=z_1}}
      \stm[2]{l_1:=\\\igaz}
      \WHEN[1]{\stm[2]{\nem l_1 \es l_2 \es \\ v[k+1] \ne z_1}}
      \stm[2]{SKIP}
      \WHEN[1]{\stm[2]{\nem l_2 \es l_1 \es \\ v[k+1]=z_2}}
      \stm[2]{l_2:=\\\igaz}
      \WHEN[1]{\stm[2]{\nem l_2 \es l_1 \es \\ v[k+1] \ne z_2}}
      \stm[2]{SKIP}
    \end{CASE}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

\end{document}
