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