def\|#1|{{\bf #1}}
\begin{tabbing}
XX\=XX\=XX\=XX\=\kill
\|function| {\tt SAT_{EX}}\,($\phi$)\\
/*  determines the set of states satisfying ${\rm EX}\,\phi$ */ \\
\|local var| $X,Y$\\
\|begin|\\
\> $X := {\tt SAT}\, (\phi);$\\
\> $Y := {\tt pre}_\exists (X);$\\
\> \|return| $Y$\\
\|end|
\end{tabbing}