\begin{frame}[fragile]{Program Variables and Logical Variables}
  \begin{definition}
    For a Hoare triple $\hoaretriple{\aform}{\aprog}{\bform}$,
    its set of \emph{logical variables} are those variables 
    that are \alert{free} in $\aform$ and $\bform$, but \alert{do not occur} in $\aprog$. 
  \end{definition}\pause{}
  
  
  \begin{exampleblock}{Examples}
  \begin{itemize}\setlength{\itemsep}{0.6ex}
    \item
      $\satisfiestot \hoaretriple{\logand{(x \ge 0)}{\equalto{\alert{x_0}}{x}}}
                                 {\forestgreen{\texttt{Fac2}}(x,y)}
                                 {y = \fac{\alert{x_0}}}$
  \pause
    \item
      $\satisfiestot \hoaretriple{\logand{x \ge 0}{\alert{x'} = x}}
                                 {\forestgreen{\texttt{Sum}}(x,z)}
                                 {z = \frac{\alert{x'} (\alert{x'}+1)}{2}}$
    
  \end{itemize}  
  \end{exampleblock}
  
  \begin{itemize}
  \pause
    \item
      called \emph{logical}: because occur only in logical formulas
  \pause
    \item
      state of program assigns a value to program variables,\\
      but not to logical variables
  \end{itemize}  
\end{frame}