\documentclass{article}
\usepackage{xcolor}
\usepackage{proof}
\usepackage{amsfonts}
\usepackage{wasysym}
\usepackage{tikz}

%% pto : -|->
%% This borrows the notation used in the zed system
\makeatletter
\newcommand{\pto}{}% just for safety
\newcommand{\pgets}{}% just for safety

\DeclareRobustCommand{\pto}{\mathrel{\mathpalette\p@to@gets\to}}
\DeclareRobustCommand{\pgets}{\mathrel{\mathpalette\p@to@gets\gets}}

\newcommand{\p@to@gets}[2]{%
  \ooalign{\hidewidth$\m@th#1\mapstochar\mkern5mu$\hidewidth\cr$\m@th#1\to$\cr}%
}
\makeatother
%% /pto}

\definecolor{dgreen}{rgb}{0,0.4,0}
\definecolor{mblue}{rgb}{0,0,0.75}

\newcommand{\Prod}{::=}
\newcommand{\dom}{\mathrel{\mathrm{dom}}}
\newcommand{\nta}[1]{\ensuremath{\textit{#1}}}
\newcommand{\ntam}[1]{\ensuremath{{#1}}}
\newcommand{\VB}{\ |\ }
\newcommand{\tuple}[1]{\ensuremath{\langle #1 \rangle}}
\newcommand{\terminal}[1]{\textit{#1}}
\newcommand{\nt}[1]{\ensuremath{\tuple{\hspace{-0.02cm}\nta{#1}\hspace{0.02cm}}}}

\newcommand{\reducedstrut}{\vrule width 0pt height .7\ht\strutbox depth .5\dp\strutbox\relax}

\newcommand{\MVCol}[2]{%    \colorbox{lgreen}{\ensuremath{#1}}%
    \begingroup%
    \setlength{\fboxsep}{0pt}%
    \colorbox{#1}{\reducedstrut\ensuremath{#2}\/}%
    \endgroup}

\newcommand{\Mid}[0]{\MV{\textit{id}}}
\newcommand{\Midi}[1]{\MV{\textit{id}_{#1}}}
\newcommand{\MV}[1]{\MVCol{green!20!white}{\textcolor{black}{#1}}}
\newcommand{\olang}[1]{\textsf{\textcolor{dgreen}{#1}}}
\newcommand{\ty}[1]{\textcolor{mblue}{#1}}
\newcommand{\rec}[1]{[#1]}
\newcommand{\Values}[0]{{\mathbb{V}}}
\newcommand{\Types}[0]{\ty{\mathbb{T}}}
\newcommand{\TInt}[0]{\ty{\textsf{\textsc{Int}}}}
\newcommand{\TNull}[0]{\ty{\textsf{\textsc{Null}}}}
\newcommand{\TUnit}[0]{\ty{\textsf{\textsc{Unit}}}}
\newcommand{\Env}[0]{\ensuremath{\mathbb{E}}}
\newcommand{\MEV}[0]{\MV{\textit{Ev}}}
\newcommand{\Ckw}[1]{\textbf{#1}}
\newcommand{\Tty}[1]{\ty{T_{#1}}}
\newcommand{\Ttrans}[0]{\mathcal{T}}
\newcommand{\assignable}[0]{\triangleleft}
\newcommand{\DatatypeInit}[0]{\mathcal{D}_0}
\newcommand{\Funenv}[0]{E_p}
\newcommand{\DatatypeTy}[0]{\mathcal{D}_T}
\newcommand{\Heap}[0]{\ensuremath{\mathbb{H}}}
\newcommand{\Ref}[0]{\textsc{Ref}}
\newcommand{\HObj}[0]{\textsc{HObj}}
\newcommand{\Anrel}[0]{\RHD}


\title{EDA045 Program Analysis, 2018, Homework \#5}

\begin{document}
\maketitle

\section*{Modalities}
\begin{itemize}
\item \textbf{Deadline}: 18 December 2018, end of day
\item \textbf{Submission mechanism}: Moodle
\item \textbf{To submit}: Your results (pdf or plaintext), including the estimated number of hours you worked on the project
\end{itemize}

In the following you will be working on a variant of ATL
(grammar: Figure~\ref{fig:atl-grammar}, semantics:
Figure~\ref{fig:atl-bigstep-opsem}, types:
Figure~\ref{fig:atl-types}), similar to the languages that we discussed in class.

If you find any obvious errors or unexpected behaviour in the
semantics, note them down and use your best judgment to decide if the
semantics need fixing.  Make sure to justify any changes that you make to the original
semantics.  I will count such fixes so as to balance out mistakes elsewhere in this assignment.

% ----------------------------------------
\begin{figure}
  \[
    \begin{array}[t]{cc}
  \begin{array}[t]{lcl}
    \nta{name} & \Prod & \terminal{id} \\
               & \VB   & \terminal{{name}\ \olang{.}\ \terminal{id}} \\
               \\
    \nta{{val}} & \Prod & \terminal{num} \\
                & \VB   & \olang{null} \\
                \\
    \nta{expr} & \Prod & \nt{val} \\
               & \VB   & \nt{expr}\olang{\texttt{+}}\nt{expr} \\
               & \VB   & \nt{name} \\
               & \VB   & \olang{print}\ \olang{(}\ \nt{val}\ \olang{)}\\
               & \VB   & \olang{new}\ \olang{(}\ \terminal{id}\ \olang{)} \\
               & \VB   & \terminal{id}\ \olang{(}\ \nt{expr}\star\ \olang{)} \\
    \\
    \nta{ty}   & \Prod & \olang{int}\\
               & | & \terminal{id}
  \end{array} &
  \begin{array}[t]{lcl}
    \nta{stmt} & \Prod & \nt{name}\ \olang{\texttt{=}}\ \nt{expr} \\
               & \VB   & \olang{\{}\ \nt{stmt}\ \olang{\}} \\
               & \VB   & \olang{if}\ \nt{{expr}}\ \nt{stmt}\ \olang{else}\ \nt{stmt} \\
               & \VB   & \olang{while}\ \nt{expr}\ \nt{stmt} \\
               & \VB   & \olang{skip} \\
               & \VB   & \olang{return}\ \nt{{expr}} \\
               & \VB   & \nt{stmt}\olang{ ; }\nt{stmt}\\
    \\
    \nta{decl} & \Prod & \olang{proc}\ \terminal{id}\ \olang{(}\ (\terminal{id}\ \olang{:}\ \nt{ty})\star\ \olang{)}\  \nt{stmt}\\
               & \VB   & \olang{datatype}\ \terminal{id} \olang{(}\ (\terminal{id}\ \olang{:}\ \nt{ty})\star\ \olang{)}\\
    \\
    \nta{prog} & \Prod & \nt{decl}\ \nt{prog} \\
               & \VB   & \nt{stmt} \\
  \end{array}\\
    \end{array}
  \]
  \caption{ATL Grammar}
  \label{fig:atl-grammar}
\end{figure}

% ----------------------------------------
\begin{figure}
  \[
  \begin{array}{r@{\hspace{0.1cm}}c@{\hspace{0.1cm}}l}
    \MV{p} & \in & \nta{prog}
    \\
    \MV{t}, \MV{t_i}  & \in & \nta{ty}
    \\
    \Mid{}, \Midi{i} & \in & \nta{id}
    \\
    \MV{n}, \MV{n_i} & \in & \nta{num}
    \\
    \MV{v}, \MV{v_i} & \in & \Values = \nta{num} \uplus \{ \olang{\Ckw{null}} \} \uplus \Ref \uplus (\nta{stmt} \times \nta{id}\star)
    \\
    \MV{e}, \MV{e_i} & \in & \nta{expr}
    \\
    \MV{s}, \MV{s_i} & \in & \nta{stmt}
    \\
    E, E', E'' & \in & \Env = \nta{id} \pto \Values
    \\
    \MEV{}& \in & \nta{val}\uplus \Env
    \\
    H, H', H'', H''', H_i & \in & \Heap = \Ref \pto \HObj
    \\
    r & \in & \Ref
    \\
    \ty{\tau}, \ty{\tau_i} & \in & \Types = \{ \TInt, \TNull, \TUnit \} \uplus \{ \Tty{\Mid} | \Mid \in \nta{id} \}
  \end{array}
  \]
  \caption{Metavariables and their domains for later definitions.}\label{fig:atl-support}
\end{figure}

% ----------------------------------------
\begin{figure}
  \[
  \begin{array}{c}
    \begin{array}{ccc}
      \mathcal{N}(\MV{t}) = \left \{
      \begin{array}{lcl}
        \olang{0} & \iff & \MV{t} = \olang{int}\\
        \olang{\Ckw{null}} &  & \textrm{otherwise}\\
      \end{array} \right .
      & \hspace{1cm} &
      \Ttrans(\MV{t}) = \left \{
      \begin{array}{lcl}
        \TInt & \iff & \MV{t} = \olang{int}\\
        \Tty{\MV{t}} & \iff & \MV{t} \in \nta{id}\\
      \end{array} \right .
      \\
    \end{array}
    \\
    \\
    \infer{
      \tuple{\DatatypeInit, \DatatypeTy, \Funenv, \MV{s}} \Anrel \tuple{\DatatypeInit, \DatatypeTy, \Funenv}
    }{}
      \\ \\
    \infer{
      \tuple{\DatatypeInit, \DatatypeTy, \Funenv, \olang{\Ckw{proc} \Mid{}(\Midi{1}\ :\ \MV{t_1}, \ldots, \Midi{k}\ :\ \MV{t_k})}\ \MV{s}\ \MV{p}} \Anrel \tuple{\DatatypeInit', \DatatypeTy', \Funenv''}
    }{
      \tuple{\DatatypeInit, \DatatypeTy, \Funenv, \MV{p}}
      \Anrel
      \tuple{\DatatypeInit', \DatatypeTy', \Funenv'}
      &
      \Mid{} \notin\ \dom \Funenv'
      &
      \Funenv'' = [\Mid \mapsto \tuple{\MV{s}, \rec{\Midi{1}, \ldots, \Midi{k}}}]\Funenv'
    }
    \\
    \\
    \infer{
      \tuple{\DatatypeInit, \DatatypeTy, \Funenv, \olang{\Ckw{datatype} \Mid{}(\Midi{1}\ :\ \MV{t_1}, \ldots, \Midi{k}\ :\ \MV{t_k})}\ \MV{p}}
      \Anrel
      \tuple{\DatatypeInit'', \DatatypeTy'', \Funenv'}
    }{
      \begin{array}{l}
        \MV{id_i} = \MV{id_k} \iff  i = k
        \\
      \tuple{\DatatypeInit, \DatatypeTy, \Funenv, \MV{p}}
      \Anrel
      \tuple{\DatatypeInit', \DatatypeTy', \Funenv'}
      \end{array}
      &
      \begin{array}{r}
      \DatatypeInit'' = [\Mid \mapsto \rec{\Midi{1}=\mathcal{N}(\MV{t_1}), \ldots, \Midi{k}=\mathcal{N}(\MV{t_k})}]\DatatypeInit'
      \\
      \DatatypeTy'' = [\Tty{\Mid} \mapsto \rec{\Midi{1}:\Ttrans(\MV{t_1}), \ldots, \Midi{k}:\Ttrans(\MV{t_k})}]\DatatypeTy'
      \end{array}
    }
  \end{array}
  \]
  \caption{ATL support definitions for deriving $\DatatypeInit$, $\DatatypeTy$, and $\Funenv$}\label{fig:atl-support}
\end{figure}

% ----------------------------------------
\begin{figure}
  \begin{tikzpicture}
    \node[draw] at (0,0) {
      \begin{minipage}{13.3cm}
        \small
        \[
        \begin{array}{c}
            \begin{array}{ccc}
              % / val --------------------
              \infer[(\textit{val})]{\tuple{H, E, \MV{v}} \Downarrow \tuple{H, \MV{v}}}{}
              % \ --------
              &\hspace{2cm}&
              % / id --------------------
              \infer[(\textit{id})]{\tuple{H, E, \Mid{}} \Downarrow \tuple{H, \MV{v}}}{E(\Mid{}) = {\MV{v}}}
              % \ --------
              \\
            \end{array}
            \\
            \\
            % / plus --------------------
            \infer[(\textit{plus})]{\tuple{E, {\MV{e_1} \texttt{+} \MV{e_2}}} \Downarrow \tuple{H'', \MV{n}}}{
              \tuple{H, E, {\MV{e_1}}} \Downarrow \tuple{H', \MV{n_1}}
              &
              \tuple{H', E, {\MV{e_2}}} \Downarrow \tuple{H'', \MV{n_2}}
              &
              \MV{n} = {\MV{n_1}} + {\MV{n_2}}
            }
            % \ --------
          \\
          \\
          % / call --------------------
          \infer[(\textit{call})]{
            \tuple{H_0, E, \olang{\Mid (\MV{e_1} \ldots \MV{e_k})}}
            \Downarrow
            \tuple{H', \MV{v}}
          } {
            \begin{array}{c}
              \\
              E({\Mid}) = \tuple{\MV{s}, [\Midi{1}, \ldots, \Midi{k}]}
            \end{array}
            &
            \begin{array}{c}
            \tuple{H_0, E, \MV{e_1}} \Downarrow \tuple{H_1, \MV{v_1}}
              \cdots
            \tuple{H_{k-1}, E, \MV{e_k}} \Downarrow \tuple{H_k, \MV{v_k}}
            \\
            \tuple{H_k, \Funenv{} \cup\{ \Midi{1}\mapsto \MV{v_1}, \cdots, \Midi{k} \mapsto \MV{v_k} \}, \MV{s}} \Downarrow \tuple{H', \MV{v}}
            \end{array}
          }
          % \ -------
          \\ \\
          % / print --------------------
          \infer[(\textit{print})]{
            \tuple{H, E, \olang{\Ckw{print}(\MV{e})}}
            \Downarrow
            \tuple{H', \olang{0}}
          } {
            \tuple{H, E, \MV{e}}
            \Downarrow
            \tuple{H', \MV{n}}
          }
          % \ -------
          \\ \\
          % / new --------------------
          \infer[(\textit{new})]{
            \tuple{H, E, \olang{\Ckw{new} (\Mid{})}}
            \Downarrow
            \tuple{H \cup \{r \mapsto [\Midi{1}\mapsto \MV{v_1}, \ldots, \Midi{k}\mapsto\MV{v_k}]\}, r}
          } { r \textit{\ fresh}
            &
            \DatatypeInit(\Mid{}) = \rec{\Midi{1}=\MV{v_1}, \ldots, \Midi{k}=\MV{v_k}}
          }
          % \ -------
          \\ \\
          % / load --------------------
          \infer[(\textit{load})]{
            \tuple{H, E, \olang{\MV{e}.\Mid}}
            \Downarrow
            \tuple{H, \MV{v}}
          } {
            \tuple{H, E, \MV{e}}
            \Downarrow
            \tuple{H, r}
            &
            H(r) = \rec{\MV{id} \mapsto \MV{v}, \ldots}
          }
          % \ -------
          \\
          \\
          % / store --------------------
          \infer[(\textit{store})]{
            \tuple{H, E, \olang{\MV{e_1}.\Mid{} = \MV{e_2}}}
            \Downarrow_s
            \tuple{[r \mapsto R']H'', E}
          } {
            \tuple{H, E, \MV{e_1}} \Downarrow \tuple{H', r}
            &
            \tuple{H', E, \MV{e_2}} \Downarrow \tuple{H'', \MV{v}}
            &
            H''(\olang{r}) = R
            &
            R' = [\Mid \mapsto \MV{v}]R
          }
          % \ -------
          \\
          \\
          \begin{array}{ccc}
          % / assign --------------------
          \infer[(\textit{assign})]
                {\tuple{H, E, \olang{\Mid{} \texttt{=} \MV{e}}} \Downarrow_s \tuple{H', [\Mid \mapsto \MV{v} ]E}}
                {\tuple{H, E, \MV{e}} \Downarrow \tuple{H', \MV{v}}}
          % \ --------
          &\hspace{0.7cm}&
          % / block --------------------
          \infer[(\textit{block})]{\tuple{H, E, \olang{\{ \MV{s} \}}} \Downarrow_s \tuple{H', E'}}{\tuple{H, E, \MV{s}} \Downarrow_s \tuple{H', E'}}
          % \ --------
          \end{array}
          \\
          \\
          \begin{array}{ccc}
          % / seq --------------------
          \infer[(\textit{seq})]{\tuple{E, \olang{ \MV{s_1}; \MV{s_2} }} \Downarrow_s \tuple{H'', \MEV{}}}{
            \tuple{H, E, \MV{s_1}} \Downarrow_s \tuple{H', E'}
            &
            \tuple{H', E', \MV{s_2}} \Downarrow_s \tuple{H'', \MEV{}}
          }
          % \ --------
          &\hspace{0.7cm}&
          % / skip --------------------
          \infer[(\textit{skip})]
                {\tuple{H, E, \olang{\Ckw{skip}}} \Downarrow_s \tuple{H, E}}
                {}
          % \ --------
          \end{array}
          \\
          \\
          % / if-then --------------------
          \infer[(\textit{if-then})]{\tuple{H, E, \olang{\Ckw{if} \MV{e} \MV{s_1} \Ckw{else} \MV{s_2}}} \Downarrow_s \tuple{H'', \MEV}}{
            \tuple{H, E, \MV{e}} \Downarrow \tuple{H', \MV{v}}
            &
            \MV{v} \in \nta{num}
            &
            \MV{v} \ne 0
            &
            \tuple{H', E, \MV{s_1}} \Downarrow_s \tuple{H'', \MEV}
          }
          % \ --------
          \\
          \\
          % / if-else --------------------
          \infer[(\textit{if-else})]{\tuple{H, E, \olang{\Ckw{if} \MV{e} \MV{s_1} \Ckw{else} \MV{s_2}}} \Downarrow_s \tuple{H'', \MEV}}{
            \tuple{H, E, \MV{e}} \Downarrow \tuple{H', \olang{0}}
            &
            \tuple{H', E, \MV{s_2}} \Downarrow_s \tuple{H'', \MEV}
          }
          % \ --------
          \\
          \\
          % / while-done --------------------
          \infer[(\textit{while-done})]
                {\tuple{H, E, \olang{\Ckw{while} \MV{e} \MV{s}}} \Downarrow_s \tuple{H', E}}
                {\tuple{H, E, \MV{e}} \Downarrow \tuple{H', \olang{0}}}
          % \ --------
          \\
          \\
          % / while-step --------------------
          \infer[(\textit{while-step})]{\tuple{H, E, \olang{\Ckw{while} \MV{e} \MV{s}}} \Downarrow_s \tuple{H''', E''}}{
            \begin{array}{l}
            \tuple{H, E, \MV{e}} \Downarrow \tuple{H', \MV{v}}
            \\
            \MV{v} \in \nta{num}
            \end{array}
            &
            \begin{array}{c}
              \\
              \MV{v} \ne 0
            \end{array}
            &
            \begin{array}{r}
            \tuple{H', E, \MV{s}} \Downarrow_s \tuple{H'', E'}
            \\
            \tuple{H'', E', \olang{\Ckw{while} \MV{e} \MV{s}}} \Downarrow_s \tuple{H''', E''}
            \end{array}
          }
          % \ --------
          \\ \\
          % / return --------------------
          \infer[(\textit{return})]{\tuple{H, E, \olang{\Ckw{return} \MV{e}}} \Downarrow_s \tuple{H', \MV{v}}}{
            \tuple{H, E, \MV{e}} \Downarrow \tuple{H', \MV{v}}
          }
          % \ -------
        \end{array}
        \]
      \end{minipage}
      };
  \end{tikzpicture}
  \caption{ATL: natural semantics, assuming that $\DatatypeInit$ and $\Funenv$ have been set up suitably (cf.\@ Figure~\ref{fig:atl-support}).}
  \label{fig:atl-bigstep-opsem}
\end{figure}

\begin{figure}
  \fbox{
    \begin{minipage}{13.3cm}\[
    \begin{array}{c}
      \begin{array}{ccccc}
      % / t-num --------------------
      \infer[(\ty{\textit{\ty{t-num}}})]
            {\Gamma \vdash \MV{v} : \TInt}{\MV{v} \in \nta{num}}
      % \ -------
            & \hspace{0.5cm} &
      % / t-null --------------------
      \infer[(\ty{\textit{\ty{t-null}}})]
            {\Gamma \vdash \olang{\Ckw{null}} : \TNull{}}{}
      % \ -------
            & \hspace{0.5cm} &
      % / t-id --------------------
      \infer[(\ty{\textit{\ty{t-id}}})]
            {\Gamma \cup \{ \Mid : \ty{\tau} \} \vdash \Mid : \ty{\tau}}{}
      % \ -------
      \\
      \end{array}
      \\
      \\
      % / t-invoke --------------------
      \infer[(\ty{\textit{\ty{t-call}}})]
            {\Gamma \vdash \olang{\Mid(\MV{e_1}, \ldots, \MV{e_k})} : \ty{\tau_0}}
            {
              \Gamma \vdash \MV{e_1} : \ty{\tau_1}
              &
              \cdots
              &
              \Gamma \vdash \MV{e_k} : \ty{\tau_k}
              &
              \Gamma \vdash F_{\Mid} : \ty{\tau_1 \times \cdots \times \tau_k \to \tau_0}
            }
      % \ -------
      \\ \\
      \begin{array}{ccc}
      % / t-plus --------------------
      \infer[(\ty{\textit{\ty{t-plus}}})]
            {\Gamma \vdash \olang{\MV{e_1} \texttt{+} \MV{e_2}} : \TInt}{
              \Gamma \vdash \MV{e_1}: \TInt
              &
              \Gamma \vdash \MV{e_2}: \TInt
            }
      % \ -------
      &\hspace{0.7cm}&
      % / t-print --------------------
      \infer[(\ty{\textit{\ty{t-print}}})]
            {\Gamma \vdash \olang{\Ckw{print}(\MV{e})} : \TInt}
            {\Gamma \vdash e : \TInt}
      % \ -------
      \end{array}
      \\ \\
      \begin{array}{ccc}
      % / t-new --------------------
      \infer[(\ty{\textit{\ty{t-new}}})]
            {\Gamma \vdash \olang{\Ckw{new}(\Mid)} : \Tty{\Mid}}
            {
              \Mid \in\ \dom \DatatypeTy
            }
      % \ -------
      &\hspace{0.7cm}&
      % / t-load --------------------
      \infer[(\ty{\textit{\ty{t-load}}})]
            {\Gamma \vdash \olang{\MV{e}.\Midi{1}} : \ty{\tau}}
            {
              \Gamma \vdash \MV{e} : \Tty{\Mid}
              &
              \DatatypeTy(\Mid) = \rec{\Midi{1}: \ty{\tau}, \ldots}
            }
      % \ -------
      \end{array}
      \\ \\
      % / t-store --------------------
      \infer[(\ty{\textit{\ty{t-store}}})]
            {\Gamma \vdash_s \olang{\MV{e_1}.\Midi{1} = \MV{e_2}} : \TUnit}
            {
              \Gamma \vdash \MV{e_1} : \Tty{\Mid}
              &
              \DatatypeTy(\Mid) = \rec{\Midi{1}: \ty{\tau}, \ldots}
              &
              \Gamma \vdash \MV{e_2} \assignable \ty{\tau}
            }
      % \ -------
      \\ \\
      \begin{array}{ccc}
      % / t-assign --------------------
      \infer[(\ty{\textit{\ty{t-assign}}})]
            {\Gamma \vdash_s \olang{\Mid{} = \MV{e}} : \TUnit}
            {
              \Gamma \vdash \Mid : \ty{\tau}
              &
              \Gamma \vdash \MV{e} \assignable \ty{\tau}
            }
      % \ -------
      &\hspace{0.7cm}&
      % / t-block --------------------
      \infer[(\ty{\textit{\ty{t-block}}})]
            {\Gamma \vdash_s \olang{\{ \MV{s} \}}: \ty{\tau}}{\Gamma \vdash_s \MV{s} : \ty{\tau}}
      % \ -------
      \\ \\
      % / t-seq --------------------
      \infer[(\ty{\textit{\ty{t-seq}}})]
            {\Gamma \vdash_s \olang{\MV{s_1}; \MV{s_2}}: \ty{\tau}}
            {
              \Gamma \vdash \MV{s_1} : \TUnit{}
              &
              \Gamma \vdash \MV{s_2} : \ty{\tau}
            }
      % \ -------
      &\hspace{0.7cm}&
      % / t-skip --------------------
      \infer[(\ty{\textit{\ty{t-skip}}})]
            {\Gamma \vdash_s \olang{\Ckw{skip}}: \TUnit}{}
      % \ -------
      \end{array}
      \\ \\
      % / t-if --------------------
      \infer[(\ty{\textit{\ty{t-if}}})]
            {\Gamma \vdash_s \olang{\Ckw{if} \MV{e_1} \MV{s_1} \Ckw{else} \MV{s_2}} : \ty{\tau}}
            {
              \Gamma \vdash \MV{e_1} : \TInt
              &
              \Gamma \vdash_s \MV{s_1} : \ty{\tau}
              &
              \Gamma \vdash_s \MV{s_2} : \ty{\tau}
            }
      % \ -------
      \\ \\
      \begin{array}{ccc}
      % / t-while --------------------
      \infer[(\ty{\textit{\ty{t-while}}})]
            {\Gamma \vdash_s \olang{\Ckw{while} \MV{e} \MV{s}} : \TUnit}
            {
              \Gamma \vdash \MV{e_1} : \TInt
              &
              \Gamma \vdash_s s : \TUnit
            }
      % \ -------
      &\hspace{0.7cm}&
      % / t-return --------------------
      \infer[(\ty{\textit{\ty{t-return}}})]
            {\Gamma \vdash_s \olang{\Ckw{return} \MV{e}}: \ty{\tau}}{\Gamma \vdash \MV{e} : \ty{\tau}}
      % \ -------
      \end{array}
      \\ \\
      % / t-proc --------------------
      \infer[(\ty{\textit{\ty{t-proc}}})]
            {
              \Gamma \vdash_s
              \olang{\Ckw{proc} \Mid{}(\Midi{1}\ :\ \MV{t_1}, \ldots, \Midi{k}\ :\ \MV{t_k})}\ \MV{s}\ \MV{p}
              : \ty{\tau}}
            {
              \begin{array}{l}
              \ty{\tau_1} = \Ttrans(\MV{t_1})
              \hspace{0.2cm}
              \cdots
              \hspace{0.2cm}
              \ty{\tau_k} = \Ttrans(\MV{t_k})
              \\
              F_{\Mid} : \ty{\tau_1 \times \cdots \times \tau_k \to \tau_0} \in \Gamma
              \\
              \end{array}
              &
              \begin{array}{r}
              \Gamma \cup \{ \Midi{1}:\ty{\tau_1}, \ldots, \Midi{k}:\ty{\tau_k} \} \vdash_s \MV{s} : \ty{\tau_0}
              \\
              \Gamma \vdash_p {\MV{p}} : \ty{\tau}
              \\
              \end{array}
            }
      % \ -------
      \\ \\
      % / t-dataty --------------------
      \infer[(\ty{\textit{\ty{t-dataty}}})]
            {
              \Gamma \vdash_s
              \olang{\Ckw{datatype} \Mid{}(\Midi{1}\ :\ \MV{t_1}, \ldots, \Midi{k}\ :\ \MV{t_k})}\ \MV{p}
              : \ty{\tau}}
            {
              \Gamma \vdash_s \MV{p} : \ty{\tau}
            }
      % \ -------
      \\ \\
      \begin{array}{ccc}
      % / assignable-ty --------------------
      \infer[(\ty{\textit{\ty{assignable-ty}}})]
            {\Gamma \vdash \olang{\MV{e}} \assignable \ty{\tau}}
            {\Gamma \vdash \olang{\MV{e}} : \ty{\tau}}
      % \ -------
      &\hspace{1cm}&
      % / assignable-null --------------------
      \infer[(\ty{\textit{\ty{assignable-null}}})]
            {\Gamma \vdash \olang{\MV{e}} \assignable \Tty{\Mid}}
            {\Gamma \vdash \olang{\MV{e}} : \TNull}
      % \ -------
      \end{array}
    \end{array}
    \]
    \end{minipage}
    } % // framebox

    \caption{ATL: type inference rules (monomorphic), assuming that $\DatatypeTy$ has been set up suitably (cf.\@ Figure~\ref{fig:atl-support}).}
  \label{fig:atl-types}
\end{figure}



\section*{\large Task \#1: Extending ATL with one primitive (0.5 points)}

Extend the ATL semantics above (which are based on the ones used in class) as follows:
\begin{itemize}
  \item Introduce a new primitive,
    $\olang{secret(}\nt{expr}\olang{)}$, which (for now) simply
    returns its parameter.  Add suitable rules to the operational
    semantics and the type system.
\end{itemize}

\section*{\large Task \#2: Dynamic Taint Analysis for ATL (2.0 points)}

Given the ATL language definition extended with the new primitive you added in Task \#1, design a dynamic taint analysis that prevents the program from printing any value
that has passed through $\olang{secret(}\nt{expr}\olang{)}$.  For example, the line
\vspace{0.3cm}

\olang{
  \begin{tabular}{l}
    print(secret(1))
  \end{tabular}
}
\vspace{0.3cm}

must result in the program getting stuck without evaluating \olang{print}.

On the other hand the following program should not result in the
program getting stuck:
\vspace{0.2cm}


\olang{
  \begin{tabular}{l}
    print(1)
  \end{tabular}
}
\vspace{0.2cm}


\begin{itemize}
\item Adjust the operational semantics of the language to prevent any data that has been returned by \olang{secret} from being printed.
  \begin{itemize}
  \item Attempt to be maximally precise.
  \item In your description, you can alter any rule in the operational semantics.
  \item If your changes systematically affect a certain set of rules, you can describe the change abstractly.  Make sure to be precise.
  \end{itemize}
\item Explain how and why your changes achieve the desired goal.
\end{itemize}

\section*{\large Task \#3: Static Taint Analysis for ATL (2.5 points)}

Given the ATL language definition extended with the new primitive you added in Task \#1, design a static taint analysis that prevents the program from printing any value
that has passed through $\olang{secret(}\nt{expr}\olang{)}$ (cf. Task~\#2  for an example).

\begin{itemize}
\item Either adjust the type system for ATL or introduce
  a new type system, approximating the dynamic analysis from Task~\#2.  Your system should be nontrivial, e.g., handle the two examples listed for Task~\#1 with full precision.
\item Explain any design tradeoffs that you have made.
\item Give an example to demonstrate how your system is optimistic or conservative.
\end{itemize}

%% \section*{Task \#1: Extending ATL with global variables (points)}


\end{document}

