\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}