\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 8. feladat}
\begin{document}
\noindent
\emph{Feladat:} Határozzuk meg az $x$ vektor elemeinek összegét úgy, hogy a páratlan indexű
elemek a negáltjukkal szerepeljenek az összegzésben!

\emph{Specifikáció:}\\
$\V = \vect(\Z, \Z)$\\
$A = \alatt{\V}{x} \times \alatt{\Z}{r} \times \alatt{\Z}{k}$\\
$B = \alatt{\V}{x'}$\\
$Q = (x=x')$\\
$R = \left( Q \es r=\sum\limits_{i=x.lob}^{x.hib} (-1)^i*x[i]\right)$

\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 = \left(Q \es k \in [x.lob-1..x.hib] \es
r=\sum\limits_{i=x.lob}^{k} (-1)^i*x[i]\right)$

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=x.lob-1 \es r=0)$

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

Tehát a program valahogy így néz ki:
\begin{stuki}
  \stm{k,r:=x.lob-1,0}
  \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=x.hib$ adódik.  Tehát $\pi = (k\ne x.hib)$.
\begin{stuki}
  \stm{k,r:=x.lob-1,0}
  \begin{WHILE}{1}{\stm{k \ne x.hib}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}

\cklharom \\
Jelen esetben ez: $(Q \es k \in [x.lob-1..x.hib-1] \es r=\cdots) \kovkerdes t>0$, tehát
a termináló függvény: $t:=x.hib-k$.  Ez a függvény $P \es \pi$
esetén nyilván pozitív.

\cklot \\
Előrevéve az utolsó feltételt már most biztosíthatjuk, hogy a programunk lefutása
véges legyen.
\begin{stuki}
  \stm{k,r:=x.lob-1,0}
  \begin{WHILE}{1}{\stm{k \ne x.hib}}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
$P\es\pi\es x.hib-k=t_0 \kovkerdes\lf(k:=k+1, x.hib-k<t_0)=
x.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)=\left(Q \es k+1 \in [x.lob-1..x.hib] \es r=\sum\limits_{i=x.lob}^{k+1} (-1)^i*x[i]\right)$
$=: Q''$, nem következik $P \es \pi$-ből (például abban az esetben, ha $x[k+1]\ne 0$.

Ezért egy szekvencia második fele lesz az eddigi ciklusmag és $Q''$-t pedig az\\
$S_{01}:=\left(r:=r+(-1)^{k+1}*x[k+1]\right)$ értékadással
érjük el a szekvencia első részében.

$P\es \pi \ekv (Q \es k \in [x.lob-1..x.hib-1] \es r=\sum\limits_{i=x.lob}^{k} (-1)^i*x[i]) \\
\kovkerdes \\
lf(S_{01}, Q'') \ekv \left(Q \es k+1 \in [x.lob-1..x.hib] \es
r+(-1)^{k+1}*x[k+1]=\sum\limits_{i=x.lob}^{k+1} (-1)^i*x[i]\right) \surd$
\begin{stuki}
  \stm{k,r:=x.lob-1,0}
  \begin{WHILE}{2}{\stm{k \ne x.hib}}
    \stm{r:=r+((-1)^{k+1}*x[k+1])}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
\end{document}