42/191
\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}