\begin{frame}[fragile,t]{Proof Rules for Partial Correctness} \begin{goal}{}\vspace{1.5ex} \begin{malign} \ruleassignment \end{malign} \end{goal} \pause\smallskip \begin{itemize} \item is best applied backwards \pause \item \alert{note} the necessity of \alert{capture avoiding} in substitution! \end{itemize} \pause \begin{goal}{} \emph{Hint} for understanding: if $\aform$ holds when replacing $x$ by $E$, then after the assignment $x = E$, the formula $\aform$ holds. \end{goal} \begin{itemize}\setlength{\itemsep}{0ex} \pause \item $\hoaretriple{\equalto{2}{y}}{\Assign{x}{2}}{\equalto{x}{y}}$ \pause \item $\hoaretriple{\equalto{2}{4}}{\Assign{x}{2}}{\equalto{x}{4}}$ \pause \item $\hoaretriple{{2}\mathrel{\dm{>}}{2}}{\Assign{x}{2}}{2\mathrel{\dm{>}}x}$ \pause \item $\hoaretriple{\equalto{x+1}{y}}{\Assign{x}{x+1}}{\equalto{x}{y}}$ \pause \item $\hoaretriple{\equalto{x + 1 + 5}{y}}{\Assign{x}{x+1}}{\equalto{x+5}{y}}$ \pause \item $\hoaretriple{x + 1 > 0 \logandinf y > 0}{\Assign{x}{x+1}}{x > 0 \logandinf y > 0}$ \end{itemize} \vspace{10cm} \end{frame}