\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 27. feladat megoldásvázlat}
\begin{document}
\noindent
\emph{Feladat:} Adott az $x$ és $b$ vektor úgy, hogy $b$ az $x$ indexeiből veszi fel elemeit.  Az $x$ vektor minden $b[j]$-edik eleme helyére írjunk nullát!

\emph{Specifikáció:}\\
$\V = \vect(\Z, \Z)$
$A = \alatt{\V}{x} \times \alatt{\V}{b} \times \alatt{\Z}{k}$\\
$B = \alatt{\V}{x'} \times \alatt{\V}{b'}$\\
$Q = ( x=x' \es b=b' \es \forall i\in[b.lob..b.hib]: b[i]\in[x.lob..x.hib])$\\
$R = ( b=b' \es \forall i\in[b.lob..b.hib]: ( b[i]\in[x.lob..x.hib] \es x[b[i]]=0 ) \\
\es \forall i\in[x.lob..x.hib]:((\not\exists k\in[b.lob..b.hib]:b[k]=i) \nyil x[i]=x'[i]) )$

\emph{Megoldás:}\\
A megoldó programot és a bizonyításhoz bevezetendő állapotok nevét ismertetjük
egy stuktogramban, azonban ezen állapotok megfoglamazását és a szükséges levezetési
szabályok feltételeinek bebizonyítását az olvasóra bízzuk.
\begin{stuki}
  \stm{k:=b.lob-1}
  \begin{WHILE}{2}{\stm{k \ne b.hib}}
    \stm{x[k+1]:=0}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
\begin{textblock}{1}(2.4,-1.60)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{1.5cm}\\$R$
\end{textblock}
\begin{textblock}{1}(10.4,-0.87)
$P \es \pi$
\vspace{0.2cm}\\$Q''$
\vspace{0.2cm}\\$P$
\end{textblock}

\end{document}