\begin{frame}[fragile,t]{Program Variables and Logical Variables}
  \vspace*{-1.25ex}
  \begin{exampleblock}{$\forestgreen{\texttt{Fac2}}$}
  \vspace*{-1.25ex}  
  \begin{lstlisting}
    y = 1;
    while (x != 0) {
      y = y * x;
      x = x - 1;
    }
  \end{lstlisting}
  \vspace*{-1.25ex}  
  \end{exampleblock}
  \pause\smallskip
  
  \mpause[1]{
  Note that $\forestgreen{\texttt{Fac2}}$ `consumes' its input:
    \begin{itemize}
      \item If $x > 0$ before execution, we have $x=0$ afterwards. 
    \end{itemize}
  }  
  \mpause{Although $\forestgreen{\texttt{Fac2}}$ computes the factorial function, we have:}
  \begin{itemize}
  \mpause{
    \item $\;{\satisfiesnotpar} \hoaretriple{x = n}{\forestgreen{\texttt{Fac2}}}{y = \fac{x}}$ \hspace*{3ex} (for $n = 2,3,\ldots$).
  }
  \mpause[?0]{
    \item
      $\malt[4]{\gray{\satisfiesparblack}}{\satisfiesnotpar} \hoaretriple{x \ge 0}{\forestgreen{\texttt{Fac2}}}{y = \fac{x}}$
  }
  \end{itemize}
  \updatepause\pause\medskip
  
  \begin{goal}{}
  Remedy: use of a \alert{logical variable} $\freevar{x_0}\,$.
  \pause
  Then we expect:
  \begin{itemize}
    \item
      $\; \satisfiespar \hoaretriple{\logand{(x \ge 0)}{\equalto{\freevar{x_0}}{x}}}
                                 {\forestgreen{\texttt{Fac2}}}
                                 {y = \fac{\freevar{x_0}}}$
  \pause
    \item
      $\; \satisfiestot \hoaretriple{\logand{(x \ge 0)}{\equalto{\freevar{x_0}}{x}}}
                                 {\forestgreen{\texttt{Fac2}}}
                                 {y = \fac{\freevar{x_0}}}$
  \end{itemize}
  \end{goal}
\end{frame}