\begin{frame}[fragile,t]{Proof Rules for Partial Correctness}
  \begin{goal}{}
    \begin{malign}
    \rulewhile[\alert]
    \end{malign}
  \end{goal}
  \pause\bigskip

  The key part is the \emph{loop invariant} \alert{$\psi$}:
  \begin{itemize}
  \pause
    \item
      the body $\aprogcxt$ of the loop usually changes the variables
  \pause
    \item
      \alert{$\psi$ expresses a relationship between values that is preserved
      by any execution of $C$}
  \pause
    \item
      the \emph{premise} expresses:
      \begin{itemize}
        \item
          if $\psi$ and $\mb{\aboolexp}$ are true before executing the body $\aprogcxt$,\\ 
          then $\psi$ will again be true afterwards 
      \end{itemize}
  \pause
    \item
      the \emph{conclusion} expresses:
      \begin{itemize}
        \item
          if $\psi$ is true before the execution,
          then no matter how often the while-loop is executed, 
          $\psi$ will also be true at the end
  \pause
        \item   
          and since the while-statement only terminates if $\mb{\aboolexp}$ does not hold any more, 
          $\mb{\aboolexp}$ will be false in the final state 
      \end{itemize}      
  \end{itemize}
\end{frame}