1201 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1202 \begin{frame}[fragile]

  1203 \mbox{}\\[-13mm]\mbox{}

  1204 

  1205 \small

  1206 \begin{center}

  1207 \bl{\begin{tabular}{lcl}

  1208 $[n]_{env}$ & $\dn$ & 

  1209 $\begin{cases}

  1210 \{+\} & \text{if}\; n > 0\\

  1211 \{-\} & \text{if}\; n < 0\\

  1212 \{0\} & \text{if}\; n = 0

  1213 \end{cases}$\\

  1214 $[x]_{env}$ & $\dn$ & $env(x)$\\

  1215 $[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} \oplus [e_2]_{env}$\\

  1216 $[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} \otimes [e_2]_{env}$\\

  1217 $[e_1 = e_2]_{env}$ & $\dn$ & $\{0, +\}$\\

  1218 \end{tabular}}

  1219 \end{center}

  1220 

  1221 \scriptsize

  1222 \begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]

  1223 def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match {

  1224   case Num(0) => Set(Zero)

  1225   case Num(n) if (n < 0) => Set(Neg)

  1226   case Num(n) if (n > 0) => Set(Pos)

  1227   case Var(x) => aenv(x)

  1228   case Plus(e1, e2) => 

  1229     aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv))

  1230   case Times(e1, e2) => 

  1231     atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv))

  1232   case Equ(e1, e2) => Set(Zero, Pos)

  1233 }

  1234 \end{lstlisting}

  1235 

  1236 \end{frame}

  1237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1238 

  1239 

  1240 

  1241 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1242   \begin{frame}[c]

  1243   \frametitle{Sign Analysis}

  1244 

  1245   \begin{itemize}

  1246   \item We want to find out whether \texttt{a} and \texttt{n}

  1247   are always positive?\medskip

  1248   \item After a few optimisations, we can indeed find this out.

  1249   \begin{itemize}

  1250   \item \texttt{if} returns \texttt{+} or \texttt{0}

  1251   \item branch into only one dircection if you know

  1252   \item if $x$ is \texttt{+}, then $x + \texttt{-1}$ 

  1253   cannot be negative 

  1254   \end{itemize}\bigskip

  1255   

  1256   \item What is this good for? Well, you do not need 

  1257   underflow checks (in order to prevent buffer-overflow

  1258   attacks).

  1259   \end{itemize}

  1260   

  1261   \end{frame}

  1262 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1263