\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 1. feladat}
\begin{document}
\noindent
\emph{Feladat:} Döntsük el a monoton növekedő $f$ függvényről a
szigorú értelemben vett monotonitást!

\emph{Specifikáció:}\\
$f:[m..n]\nyil\Z$ \\
$A = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\Z}{l}$\\
$B = \alatt{\Z}{m'} \times \alatt{\Z}{n'}$\\
$Q = ( m=m' \es n=n' \es m\le n \es \forall i\in[m..n-1]: f(i)\le f(i+1))$\\
$R = ( Q \es l=(\forall i\in [m..n-1]: f(i)<f(i+1))) = (Q \es \nem l=(\exists i\in [m..n-1]: f(i)\ge f(i+1)))$

Ha az utófeltétel második alakját vesszük figyelembe, akkor a
specifikáció hasonlít a lin. ker. 2.8 specifikációjához, pár apró
eltéréstől eltekintve.  Ilyen eltérés (a táblázatban
összefoglalhatókon kívűl), hogy a tétel $i$ állapottérkomponense a mi
specifikációnkban nem szerepel, illetve az, hogy a tétel nem követelné
meg a vizsgált függvény monotonitását.  Tehát egyrészről $i$ szerint
általánosított alteres, másrészről -- az előfeltételek különbözősége
miatt -- általánosított ez a visszavezetés.

\begin{tabular}{cccr}
  feladat &  & lin. ker. 2.8 \\
  \hline
  $f(i)\ge f(i+1)$ & \knyil & $\beta(i)$ \\
  $\nem l$ & \knyil & $l$ \\
  $n-1$ & \knyil & $n$
\end{tabular}

\begin{stuki}
  \stm{i,\nem l:=m-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem \nem l \es i \ne n-1}}
    \stm{\nem l:=f(i+1)\ge f(i+2)}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

Ezzel a struktogrammal több probléma is van.  A legnagyobb az, hogy
szerepelnek benne nem megengedett értékadások.  Hiszen az értékadás
definíciójakor a jelölésben csak azt engedtük meg, hogy a bal oldalon
változónevek álljanak.  Itt azonban egy kifejezés, nevezetesen a $\nem
l$ áll, ahol $l$ már változónév.  Egyszerű meggondolások alapján
azonban láthatjuk, hogy az ilyen típusú értékadások átírhatók
érvényessé, ha ``mindkét oldalt mégegyszer tagadjuk'', majd a
kialakult $\nem \nem l$ formulák helyére egyszerűen csak $l$-et írunk.
Ezzel az utolsó lépéssel a stuktogram másik fölösleges alakú
kifejezését, a benne szereplő $\nem \nem l$ részt is kiküszöböltük.

Így:
\begin{stuki}
  \stm{i,l:=m-1,\igaz}
  \begin{WHILE}{2}{\stm{l \es i \ne n-1}}
    \stm{l:=f(i+1)<f(i+2)}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}


\end{document}