\begin{frame}[fragile,t]{Partial and Total Correctness}
  A roundabout implementation of the successor function:  
  \begin{exampleblock}{$\forestgreen{\texttt{Succ}}$}
  \begin{lstlisting}
    a = x + 1;
    if (a - 1 == 0) {
        y = 1;
    } else {
        y = a;
    }         
  \end{lstlisting}
  \end{exampleblock}
  \pause\bigskip

  We should be able to prove:
  \begin{itemize}
  \pause
    \item
      $\satisfiespar \hoaretriple{\true}{\forestgreen{\texttt{Succ}}}{y = x + 1}$
  \pause
    \item
      $\satisfiestot \hoaretriple{\true}{\forestgreen{\texttt{Succ}}}{y = x + 1}$
  \end{itemize}
\end{frame}