\begin{frame}[fragile,t]{Proof Rules for Partial Correctness} \begin{goal}{} \begin{malign} \ruleif \end{malign} \end{goal} \pause\bigskip The goal (conclusion) is decomposed into two subgoals: \begin{itemize} \pause\medskip \item if $\mb{\aboolexp}$ evaluates to true, the then-part $\aprogcxti{1}$ is executed \pause\medskip \item if $\mb{\aboolexp}$ evaluates to false, the else-part $\aprogcxti{2}$ is executed \end{itemize} \pause\medskip In both cases, $\bform$ has to hold after the execution. \vspace{10cm} \end{frame}