103/191
\begin{frame}[fragile,t]{Total Correctness}
  \vspace*{-1.2ex}
  \tcorrect{}
  \pause
  
  \vspace*{-0.95ex}
  \begin{exampleblock}{}
    \begin{itemize}\setlength{\itemsep}{0pt}
      \item
        $\malt[1]{\gray{\satisfiestotblack}}{\satisfiestot}
         \hoaretriple{\formula{x > 0}}
                     {\WhileDo{(x > 0)}{\Assign{x}{x - 1}}}
                     {\formula{\equalto{x}{0}}}$
    \updatepause
      \item
        $\malt[1]{\gray{\satisfiestotblack}}{\satisfiestot}
         \hoaretriple{\formula{x = 0}}
                     {\WhileDo{(x > 0)}{\Assign{x}{x - 1}}}
                     {\formula{\equalto{x}{0}}}$
    \updatepause
      \item
        $\malt[1]{\gray{\satisfiestotblack}}{\satisfiesnottot}
         \hoaretriple{\formula{x < 0}}
                     {\WhileDo{(x > 0)}{\Assign{x}{x - 1}}}
                     {\formula{\equalto{x}{0}}}$
    \updatepause
      \item
        $\malt[1]{\gray{\satisfiestotblack}}{\satisfiesnottot}
         \hoaretriple{\formula{\true}}
                     {\WhileDo{(x > 0)}{\Assign{x}{x - 1}}}
                     {\formula{\equalto{x}{0}}}$
    \updatepause
      \item
        $\malt[1]{\gray{\satisfiestotblack}}{\satisfiesnottot}
         \hoaretriple{\formula{\true}}
                     {\WhileDo{\boolfalse}{\Assign{x}{x - 1}}}
                     {\formula{\equalto{x}{0}}}$
    \updatepause
      \item
        $\malt[1]{\gray{\satisfiestotblack}}{\satisfiesnottot}
         \hoaretriple{\formula{\true}}
                     {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                     {\formula{\equalto{x}{0}}}$
    \updatepause
      \item
        $\malt[1]{\gray{\satisfiestotblack}}{\satisfiesnottot}
         \hoaretriple{\aform}
                     {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                     {\bform}$
    \end{itemize}
  \end{exampleblock}
\end{frame}