\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 11. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adott a $t$ négyzetes mátrix. Határozzuk meg az alsó háromszög
elemeinek összegét!

\emph{Specifikáció:}\\
$\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} \times \alatt{\Z}{r} \times \alatt{\Z}{k} \times \alatt{\Z}{g}$\\ 
$B = \alatt{\M}{t'}$\\
$Q = (t=t')$\\
$R = \left(Q \es r=\sum\limits_{i=t.lob}^{t.hib} \sum\limits_{j=t.lob}^{i} {t_i}_j\right)$

\emph{Megoldás:}\\
A megoldó ciklus invariánsa:\\
$P = \left(Q \es k\in[t.lob-1..t.hib] \es r=\sum\limits_{i=t.lob}^{k} \sum\limits_{j=t.lob}^i {t_i}_j\right)$

Ellenőrízzük le a ciklus feltételeit:\\
\cklegy \\
$Q' = (Q \es k=t.lob-1 \es r=0)$

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

\cklketto \\
$P$ és $R$ összehosonlításából $\nem\pi$-re $k=t.hib$ adódik.  Tehát $\pi = (k\ne t.hib)$.
\begin{stuki}
  \stm{k,r:=t.lob-1,0}
  \begin{WHILE}{1}{\stm{k \ne t.hib}}
    \stm{\dots}
  \end{WHILE}
\end{stuki}

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

\cklnegyot \\
Ezt a pontot a szokásos alakú ciklusmaggal biztosítjuk, ami egy szekvencia.  A szekvencia
második utasítása a ciklusváltozót növeli.

$Q''= (\lf(k:=k+1, P) \es t=t_0) = 
\left(Q \es k+1\in[t.lob-1..t.hib] \es r=\sum\limits_{i=t.lob}^{k+1} \sum\limits_{j=t.lob}^i {t_i}_j\right) \es t=t_0$

A szekvencia első része a
$P \es \pi \es t=t_0 \kov \lf(S_{01}, Q'')$ feltételt kell teljesítse!  Nézzük közelebbről ezt a feltételt ($S_{01}$-et egyelőre SKIP-nek tekintve):\\
$\left(Q \es k \in [t.lob-1..t.hib-1] \es r=\sum\limits_{i=t.lob}^k \sum\limits_{j=t.lob}^i {t_i}_j\right) \es t=t_0 \kovkerdes \\xo
\left(Q \es k+1 \in [t.lob-1..t.hib] \es r=\sum\limits_{i=t.lob}^{k+1} \sum\limits_{j=t.lob}^i {t_i}_j\right) \es t=t_0
\ekv\\\ekv
\left(Q \es k+1 \in [t.lob-1..t.hib] \es r=(\sum\limits_{i=t.lob}^k \sum\limits_{j=t.lob}^i {t_i}_j) + \sum\limits_{j=t.lob}^{k+1} {t_{k+1}}_j\right) \es t=t_0$

$S_{01}$ nem lehet egyetlen értékadás, mert akkor a nem megengedett szummát kellene
használni a jobb oldalán.  A $P \es \pi \es t=t_0$ és a $Q''$ állapot összekötésére egy ciklus
alkalmas. Az invariánsát úgy kapjuk, hogy a $Q''$-ben a második szumma hatáskörét
csökkentjük: \\
$P'= ( Q \es k+1 \in [t.lob-1..t.hib] \es g\in [t.lob-1..k+1] \es r=(\sum\limits_{i=t.lob}^k \sum\limits_{j=t.lob}^i {t_i}_j) + \sum\limits_{j=t.lob}^{g} {t_{k+1}}_j \es t=t_0) $

A belső ciklus levezetéséhez szükséges további állapotok:\\
$Q''' = ( Q \es k+1 \in [t.lob-1..t.hib] \es g=t.lob-1 \es r=(\sum\limits_{i=t.lob}^k \sum\limits_{j=t.lob}^i {t_i}_j) \es t=t_0 )$,\\
$Q^* = ( Q \es k+1 \in [t.lob-1..t.hib] \es g+1\in [t.lob-1,k+1] \es
  r=(\sum\limits_{t.lob=1}^k \sum\limits_{j=t.lob}^i {t_i}_j) + \sum\limits_{j=t.lob}^{g+1} {t_{k+1}}_j)$.

\begin{stuki}[6cm]
  \stm{k,r:=t.lob-1,0}
  \begin{WHILE}{5}{\stm{k \ne t.hib}}
    \stm{g:=t.lob-1}
    \begin{WHILE}{2}{\stm{g \ne k+1}}
      \stm{r:=r+{t_{k+1}}_{g+1}}
      \stm{g:=g+1}
    \end{WHILE}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
\begin{textblock}{1}(3.8,-2.64)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{3.4cm}\\$R$
\end{textblock}
\begin{textblock}{1}(8.9,-1.94)
$P \es \pi$
\vspace{0.2cm}\\$Q'''$
\vspace{0.2cm}\\$P' \es \pi'$
\vspace{0.2cm}\\$Q^*$
\vspace{0.2cm}\\$Q''$
\end{textblock}
\end{document}