\begin{frame}[fragile,t]{Proof Rules for Partial Correctness} \begin{goal}{} \begin{malign} \rulecomposition \end{malign} \end{goal} \pause\medskip Convenient to read bottom up (also for the other rules): \pause\medskip In order to prove \begin{talign} \hoaretriple{\aform}{\SeqComp{\aprogcxti{1}}{\aprogcxti{2}}}{\bform} \end{talign} \pause we need to find an \emph{appropriate midcondition} $\eform$, and prove \begin{talign} & \hoaretriple{\aform}{\aprogcxti{1}}{\eform} & & \text{ and } & & \hoaretriple{\eform}{\aprogcxti{2}}{\bform} \end{talign} \pause We thereby split the goal into two subgoals: \begin{itemize}\vspace*{0.3ex}\setlength{\itemsep}{0.3ex} \item execution of $\aprogcxti{1}$ in a state satisfying $\aform$,\\ we get to a state satisfying $\eform$ \item execution of $\aprogcxti{2}$ in a state satisfying $\eform$,\\ we get to a state satisfying $\bform$ \end{itemize} \vspace{10cm} \end{frame}