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