\begin{frame}[fragile,t]{Proof Rules for Partial Correctness} \begin{goal}{}\vspace{1.5ex} \begin{malign} \ruleassignment \end{malign} \end{goal} \pause\bigskip \begin{exampleblock}{} For $\psi$ is $\equalto{x}{5}$ we get:\pause \begin{talign} \hoaretriple{\equalto{6}{5}} {\Assign{x}{6}} {\equalto{x}{5}} \end{talign} \pause{} For $\psi'$ is $\equalto{x}{6}$ we get: \begin{talign} \hoaretriple{\equalto{6}{6}} {\Assign{x}{6}} {\equalto{x}{6}} \end{talign} \end{exampleblock} \pause\medskip \begin{alertblock}{} The reverse form with conclusion \begin{talign} \hoaretriple{\bform} {\Assign{x}{\aexp}} {\substforin{\aexp}{x}{\bform}} \end{talign} does not make sense! \pause E.g.\ for $\aform$ is $\equalto{x}{5}$ it would entail: \begin{talign} \hoaretriple{\equalto{x}{5}} {\Assign{x}{6}} {\equalto{6}{5}} \quad \alert{\xmark} \end{talign} \end{alertblock} \vspace{10cm} \end{frame}