\begin{frame}[fragile,t]{Program Variables and Logical Variables}
  \vspace*{-1.25ex}
  $\forestgreen{\texttt{Sum}}$ adds up the first $x$ natural numbers and stores them in $z\,$:
  \begin{exampleblock}{$\forestgreen{\texttt{Sum}}$}
  \vspace*{-1.25ex}  
  \begin{lstlisting}
    z = 0;
    while (x > 0) {
      z = z + x;
      x = x - 1;
    }  
  \end{lstlisting}
  \vspace*{-1.25ex}    
  \end{exampleblock}
  \pause\smallskip
  
  During execution $x$ is consumed.
  \pause 
  So while we have e.g.:
  \begin{itemize}
    \item $\satisfiestot \hoaretriple{x = 2}{\forestgreen{\texttt{Sum}}}{z = 3}$,
  \pause
    \item $\satisfiestot \hoaretriple{x = 3}{\forestgreen{\texttt{Sum}}}{z = 6}$,
  \end{itemize}
  \pause
  we find:
  \begin{itemize}
    \item
      $\satisfiesnottot \hoaretriple{x \ge 0}{\forestgreen{\texttt{Sum}}}{z = \frac{x (x+1)}{2}}$,
      \hspace*{2ex}
      (note: $\sum_{i=1}^{x} i = \frac{x (x+1)}{2}$).\pause{} 
  \end{itemize}

  \begin{goal}{}
    Again, we `store' the initial value of $x$ in a logical variable $\freevar{x_0}$:
    \begin{itemize}
      \item
        $\satisfiestot \hoaretriple{\logand{x \ge 0}{\freevar{x_0} = x}}{\forestgreen{\texttt{Sum}}}{z = \frac{\freevar{x_0} (\freevar{x_0}+1)}{2}}$
    \end{itemize}    
  \end{goal}
\end{frame}