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