\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{Answer}
\begin{popup}
\subsection*{Answer}

Let $Truth$ be the algorithm with a single variable $t$ initialized to
\TRUE\ and whose body is
\begin{display}
\textbf{while (} \TRUE\ \textbf{) \{} $t := \TRUE$ \textbf{\}}
\end{display}
Formula $I$ is an invariant of $S$ iff $S$ implements $Truth$
under the refinement mapping $\ov{t}\,\deq\, I$.
\end{popup}
\makepopup