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