\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}