\begin{frame}[fragile,t]{Program \texttt{Sum}}
  Computing the sum of the first $x$ natural numbers.
  
  \begin{exampleblock}{Program {\tt Sum}}  
  \begin{lstlisting}
    z = 0;
    while (x > 0) {
      z = z + x;
      x = x - 1;
    }  
  \end{lstlisting}
  \end{exampleblock}
  \pause\bigskip
  
  \malt[1]{
    Note that:
    \begin{talign}
      \displaystyle\sum_{i=1}^{x} i \; & =\; 1 + 2 + 3 + \ldots + x \\[-1ex]
      & =\; \frac{x (x+1)}{2}
    \end{talign}
  }{
    \pause
    We would like to express, for example:
    \begin{itemize}
    \pause
      \item
        started with input $\forestgreen{x} \ge 0 $,\;
        \texttt{Sum} yields output $\sum_{i=1}^{\forestgreen{x}} i$ for z
    \pause
      \item
        on every input value, \texttt{Sum} terminates
    \end{itemize}
    \pause
    These are \emph{program specifications} (satisfied by \texttt{Sum}). 
  }
\end{frame}