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