\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 7. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adottak az $x$ és $y$ vektorok (x.dom=y.dom).  Képezzük
az x+y és x-y vektorok skaláris szorzatát!

\emph{Specifikáció:}\\
$\V = \vect(\cH, \Z)$\\
$A = \alatt{\V}{x} \times \alatt{\V}{y} \times \alatt{\Z}{r} \times \alatt{\N_0}{k}$\\
$B = \alatt{\V}{x'} \times \alatt{\V}{y'}$\\
$Q = (x=x' \es y=y' \es x.dom=y.dom)$\\
$R = ( Q \es r=\sum\limits_{i=0}^{x.dom-1} (x_{succ^i(x.lob)}+y_{succ^i(y.lob)})*(x_{succ^i(x.lob)}-y_{succ^i(y.lob)}))$

\emph{Megoldás:}\\
A megoldó ciklus invariánsa:

$P = (Q \es k \in [0..x.dom] \es r=\sum\limits_{i=0}^{k-1}(x_{succ^i(x.lob)}+y_{succ^i(y.lob)})*(x_{succ^i(x.lob)}-y_{succ^i(y.lob)}))$

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

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

\cklketto \\
$\pi = (k\ne x.dom)$.

A program eddig így néz ki:
\begin{stuki}
  \stm{k,r:=0,0}
  \begin{WHILE}{1}{\stm{k\ne x.dom}}
    \stm{S_2}
  \end{WHILE}
\end{stuki}

\cklharom \\
Jelen esetben ez: $(Q \es k \in [0..x.dom-1] \es r=\cdots)\kov t>0$, tehát a \\
$t=x.dom-k$ függvény egy megfelelő terminálófüggvény.

\cklnegyot \\
Szekvencia legyen az $S_2$, közbülső állapot:\\
$Q'' = ( \lf(k:=k+1, P) \es t=t_0 ) = ( Q \es k+1 \in [0..x.dom] \es $\\
$\es r=\sum\limits_{i=0}^{k}(x_{succ^i(x.lob)}+y_{succ^i(y.lob)})*(x_{succ^i(x.lob)}-y_{succ^i(y.lob)}))
\es t=t_0 )$

$P\es\pi\es t=t_0 \kovkerdes \lf(r:=r+(x_{succ^k(x.lob)}+y_{succ^k(y.lob)})*(x_{succ^k(x.lob)}-y_{succ^k(y.lob)}), Q'') \surd$\\
$Q''= (\lf(k:=k+1, P) \es t=t_0 \kovkerdes \lf(k:=k+1, P \es t<t_0) = \lf(k:=k+1, P) \es
\underbrace{\lf(k:=k+1, t<t_0)}_{x.dom-k-1<t_0}) \surd$

\begin{stuki}[11cm]
  \stm{k,r:=0,0}
  \begin{WHILE}{2}{\stm{k\ne x.dom}}
    \stm{r:=r+(x_{succ^k(x.lob)}+y_{succ^k(y.lob)})*(x_{succ^k(x.lob)}-y_{succ^k(y.lob)})}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

Megjegyzés: ha nem tekintjük megengedett műveletnek a programban a $succ$ valamelyik hatványára
való hivatkozást, akkor a kérdéses függvényeket helyettesíthetjük változóval, ekkor az alábbi
programot kapjuk:

\begin{stuki}
  \stm{xi,yi,r,k:=x.lob,y.lob,0,0}
  \begin{WHILE}{2}{\stm{k\ne x.dom}}
    \stm{r:=r+(x_{xi}+y_{yi})*(x_{xi}-y_{yi})}
    \stm{k,xi,yi:=k+1,succ(xi),succ(yi)}
  \end{WHILE}
\end{stuki}

Továbbá, ha a vektort (kevésbé általános módon) $\vect(\Z, \Z)$ alakúnak
képzeljük, akkor a $succ^i(x.lob)$ kifejezéshez hasonló formulák összeadásra,
azaz $x.lob+i$ alakúra egyszerűsödnek:

\begin{stuki}[8cm]
  \stm{k,r:=0,0}
  \begin{WHILE}{3}{\stm{k \ne x.dom}}
    \stm[2]{r:=r+(x_{x.lob+k}+y_{y.lob+k})*\\*(x_{x.lob+k}-y_{y.lob+k})}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}

\end{document}