\begin{frame}[fragile,t]{Partial and Total Correctness}
  \vspace*{-1ex}  
  \begin{exampleblock}{\forestgreen{\tt Fac1}}
  \vspace*{-1.25ex}                     
  \begin{lstlisting}
    y = 1;
    z = 0;
    while (z != x) {
      z = z + 1;
      y = y * z;
    }
  \end{lstlisting}
  \vspace*{-1.25ex}
  \end{exampleblock}
  
  Does not terminate for $x < 0\,$!
  \pause\medskip
  
  Therefore for total correctness, we expect to be able to prove:
  \begin{itemize}
  \pause
    \item $\satisfiesnottot \hoaretriple{\formula{\true}}{\forestgreen{\texttt{Fac1}}}{\formula{y = \fac{x}}}$
  \pause
    \item $\satisfiestot \hoaretriple{\formula{x \ge 0}}{\forestgreen{\texttt{Fac1}}}{\formula{y = \fac{x}}}$
  \end{itemize}
  \pause\medskip
  
  And for partial correctness we expect:
  \begin{itemize}
  \pause
    \item $\satisfiespar \hoaretriple{\formula{x \ge 0}}{\forestgreen{\texttt{Fac1}}}{\formula{y = \fac{x}}}$
  \pause
    \item $\satisfiespar \hoaretriple{\formula{\true}}{\forestgreen{\texttt{Fac1}}}{\formula{y = \fac{x}}}$
  \end{itemize}
\end{frame}