\begin{tabbing}
XX\=XX\=XX\=XX\=\kill
\|function| \text{{\tt SAT}$_{\text{EG}}$}\,($\phi$)\\
/*  determines the set of states satisfying $\text{EG}\, \phi$ */ \\
\|local var| $X,Y$\\
\|begin|\\
\> $Y := {\tt SAT}\,(\phi);$\\
\> $X := \emptyset;$\\
\> \|repeat until| $X=Y$\\
\> \|begin|\\
\> \> $X := Y$;\\
\> \> $Y := Y \cap {\tt pre}_\exists (Y)$\\
\> \|end|\\
\> \|return| $Y$\\
\|end|
\end{tabbing}