\begin{frame}[fragile]{Hoare Triples (Examples)}
  \begin{exampleblock}{Factorial computing program \forestgreen{\tt Fac1}}
  \begin{lstlisting}
    y = 1;
    z = 0;
    while (z != x) {
      z = z + 1;
      y = y * z;
    }
  \end{lstlisting}
  \end{exampleblock}
  \pause\medskip
  
  Does \texttt{Fac1} always terminate?\pause\ ---~\alert{Not for $x < 0\,$!}
  \pause\bigskip

  Therefore \texttt{Fac1}:
  \begin{itemize}
  \pause
    \item cannot (totally) satisfy the specification (\alert{Hoare triple})
         \begin{talign}
           \hoaretriple{\formula{\true}}{\forestgreen{\aprog}}{\formula{y = \fac{x}}}
         \end{talign}
  \pause\vspace{-3ex}
    \item but it can   satisfy: 
          \begin{talign}
            \hoaretriple{\formula{x \ge 0}}{\aprog}{\formula{y = \fac{x}}}
          \end{talign}
  \end{itemize}
  \vspace{10cm}
\end{frame}