\begin{frame}[fragile]{Simple Core Language (Syntax, Operational Meaning)}
  \begin{goal}{}
    Commands:
    \begin{talign}
      \aprogcxt \;\; {::=}  \;\; &
        \underbrace{ 
          \Assign{x}{\aexp}\phantom{\raisebox{-1ex}{}} 
        }_{{\parbox{8ex}{\scriptsize\centering atomic\\ command}}}  
          \;\mid\;     
        \underbrace{ 
          \SeqComp{\aprogcxt}{\aprogcxt}
            \;\mid\;
          \IfThenElse{\aboolexp}{\aprogcxt}{\aprogcxt}
            \;\mid\;
          \WhileDo{\aboolexp}{\aprogcxt}\phantom{\raisebox{-1ex}{}}
        }_{{\text{control structures}}}
    \end{talign}
  \end{goal}
  \pause\bigskip
  
  \malt[7]{
    \alert{Assignment statement} $\mb{\Assign{x}{\aexp}}$:
    \begin{enumerate}[(a)]\setlength{\itemsep}{.5ex}
    \pause
      \item evaluates integer expression $\mb{\aexp}$ in current state
    \pause
      \item overwrites current value stored in $\mb{x}$ by that result
    \end{enumerate}
    \pause\bigskip
  
    \alert{Sequential composition} $\SeqComp{\aprogcxti{1}}{\aprogcxti{2}}$:
    \begin{enumerate}[(a)]\setlength{\itemsep}{.5ex}
    \pause
      \item begins with executing $\aprogcxti{1}$
    \pause
      \item if this does not terminate,\\\hspace*{1.5ex} then the run of $\SeqComp{\aprogcxti{1}}{\aprogcxti{2}}$ does not terminate
    \pause
      \item otherwise the run continues by executing $\aprogcxti{2}$\\\hspace*{1.5ex}
            in the (storage) state resulting from the execution of $\aprogcxti{1}$     
    \end{enumerate}
  }{
    \mpause[-1]{}
    \updatepause
    \alert{If-then-else statement} $\IfThenElse{\mb{\aboolexp}}{\aprogcxti{1}}{\aprogcxti{2}}$:
    \begin{enumerate}[(a)]\setlength{\itemsep}{.5ex}
    \pause
      \item evaluates boolean expression $\mb{\aboolexp}$ in the current state
    \pause
      \item if the result is true, then $\aprogcxti{1}$ is executed;
    \pause
      \item otherwise $\aprogcxti{2}$ is executed.
    \end{enumerate}
    \pause\bigskip
    
    \alert{While-do statement} $\WhileDo{\mb{\aboolexp}}{\aprogcxt}$:
    \begin{enumerate}[(a)]\setlength{\itemsep}{.5ex}
    \pause
      \item boolean expression $\mb{\aboolexp}$ is evaluated in the current state
    \pause
      \item if $\mb{\aboolexp}$ evaluates to false, then the command terminates
    \pause
      \item otherwise, command $\aprogcxt  $ will be executed.
    \pause
      \item if that execution terminates, then we resume at \mb{(a)}
    \end{enumerate}
  }
  \vspace{10cm}
\end{frame}