\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