Describe types, values, rough semantics

This commit is contained in:
Théophile Bastian 2018-03-04 17:39:18 +01:00
parent ef87d28135
commit 7ad40c8cf3

View file

@ -25,6 +25,10 @@
\newcommand{\actions}{\mathbb{A}} \newcommand{\actions}{\mathbb{A}}
\newcommand{\commands}{\mathbb{C}} \newcommand{\commands}{\mathbb{C}}
\newcommand{\askip}{\operatorname{skip}} \newcommand{\askip}{\operatorname{skip}}
\newcommand{\stores}{\operatorname{Store}}
\newcommand{\states}{\operatorname{State}}
\newcommand{\traces}{\operatorname{Trace}}
\newcommand{\state}[2]{\langle{} #1, #2 \rangle{}}
\newcommand*\oldmacro{}% \newcommand*\oldmacro{}%
\let\oldmacro\insertshorttitle% \let\oldmacro\insertshorttitle%
@ -163,6 +167,59 @@
\end{columns} \end{columns}
\end{frame} \end{frame}
\begin{frame}{Types, rough semantics}
\hspace*{-1em}\textbf{Types \& values}
\begin{columns}[c]
\column{0.6\textwidth}
\begin{itemize}
\item $\values\,:=\,\relset \cup \set{a, \ldots, z}^\ast$
\item Types: Int, String, Undef, $\emptyset$, $\Omega$
\item Undef: error type
\end{itemize}
\column{0.4\textwidth}
\begin{center}
\begin{tikzpicture}{c}
\node (E) at (0, 0) {$\emptyset$};
\node (I) at (-1.5, 1) {Int};
\node (S) at (0, 1) {String};
\node (U) at (1.5, 1) {Undef};
\node (T) at (0, 2) {$\Omega$};
\draw[->] (E) -- (I);
\draw[->] (E) -- (S);
\draw[->] (E) -- (U);
\draw[<-] (T) -- (I);
\draw[<-] (T) -- (S);
\draw[<-] (T) -- (U);
\end{tikzpicture}
\end{center}
\end{columns}
\vspace{1em}
\hspace*{-1em}\textbf{Semantics}
\begin{columns}[c]
\column{.5\textwidth}
\begin{itemize}
\item Type-dependant $+$:
\begin{itemize}
\item $+_{String}$: concatenation
\item $+_{Int}$: usual $+$
\item $+_{Str, Int}$: yields Undef
\end{itemize}
\end{itemize}
\column{.5\textwidth}
\begin{align*}
\stores &:= \vars \to \values & \rho \\
\states &:= \commands \times \stores & \state{C}{\rho} \\
\traces &:= \states^\ast
\end{align*}
\end{columns}
\end{frame}
\section{Abstract interpretation} \section{Abstract interpretation}
\begin{frame}{AbsInt hot path extraction} \begin{frame}{AbsInt hot path extraction}